Package natural-prime-def: Definition of prime natural numbers

Information

namenatural-prime-def
version1.43
descriptionDefinition of prime natural numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-10-30
checksum7d7f0fefae5f3712431fdb6bd9689503b4102de5
requiresbool
natural
natural-divides
showData.Bool
Number.Natural

Files

Defined Constant

Theorem

p. prime p ¬(p = 1) n. divides n p n = 1 n = p

External Type Operators

External Constants

Assumptions

() = λp. p = λx.