Prime numbers #
This file deals with prime numbers: natural numbers p ≥ 2
whose only divisors are p
and 1
.
Important declarations #
Nat.Prime
: the predicate that expresses that a natural numberp
is primeNat.Primes
: the subtype of natural numbers that are primeNat.minFac n
: the minimal prime factor of a natural numbern ≠ 1
Nat.prime_iff
:Nat.Prime
coincides with the general definition ofPrime
Nat.irreducible_iff_nat_prime
: a non-unit natural number is only divisible by1
iff it is prime
A copy of not_prime_zero
stated in a way that works for aesop
.
See https://github.com/leanprover-community/aesop/issues/197 for an explanation.
A copy of not_prime_one
stated in a way that works for aesop
.
See https://github.com/leanprover-community/aesop/issues/197 for an explanation.
This instance is set up to work in the kernel (by decide
) for small values.
Below (decidablePrime'
) we will define a faster variant to be used by the compiler
(e.g. in #eval
or by native_decide
).
If you need to prove that a particular number is prime, in any case
you should not use by decide
, but rather by norm_num
, which is
much faster.
Equations
If n < k * k
, then minFacAux n k = n
, if k | n
, then minFacAux n k = k
.
Otherwise, minFacAux n k = minFacAux n (k+2)
using well-founded recursion.
If n
is odd and 1 < n
, then minFacAux n 3
is the smallest prime factor of n
.
By default this well-founded recursion would be irreducible.
This prevents use decide
to resolve Nat.prime n
for small values of n
,
so we mark this as @[semireducible]
.
In future, we may want to remove this annotation and instead use norm_num
instead of decide
in these situations.
Equations
Instances For
This definition is faster in the virtual machine than decidablePrime
,
but slower in the kernel.
Equations
Instances For
Alias of the reverse direction of Nat.prime_iff
.
Alias of the forward direction of Nat.prime_iff
.