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.min_fac n
: the minimal prime factor of a natural numbern ≠ 1
nat.exists_infinite_primes
: Euclid's theorem that there exist infinitely many prime numbers. This also appears asnat.not_bdd_above_set_of_prime
andnat.infinite_set_of_prime
.nat.factors n
: the prime factorization ofn
nat.factors_unique
: uniqueness of the prime factorisationnat.prime_iff
:nat.prime
coincides with the general definition ofprime
nat.irreducible_iff_prime
: a non-unit natural number is only divisible by1
iff it is prime
prime p
means that p
is a prime number, that is, a natural number
at least 2 whose only divisors are p
and 1
.
Equations
- nat.prime p = irreducible p
Instances for nat.prime
This instance is slower than the instance decidable_prime
defined below,
but has the advantage that it works in the kernel for small values.
If you need to prove that a particular number is prime, in any case
you should not use dec_trivial
, but rather by norm_num
, which is
much faster.
Equations
- p.decidable_prime_1 = decidable_of_iff' (2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p) nat.prime_def_lt'
If n < k * k
, then min_fac_aux n k = n
, if k | n
, then min_fac_aux n k = k
.
Otherwise, min_fac_aux n k = min_fac_aux n (k+2)
using well-founded recursion.
If n
is odd and 1 < n
, then then min_fac_aux n 3
is the smallest prime factor of n
.
Equations
- n.min_fac_aux k = ite (n < k * k) n (ite (k ∣ n) k (n.min_fac_aux (k + 2)))
This instance is faster in the virtual machine than decidable_prime_1
,
but slower in the kernel.
If you need to prove that a particular number is prime, in any case
you should not use dec_trivial
, but rather by norm_num
, which is
much faster.
Equations
- p.decidable_prime = decidable_of_iff' (2 ≤ p ∧ p.min_fac = p) nat.prime_def_min_fac
A version of nat.exists_infinite_primes
using the bdd_above
predicate.
A version of nat.exists_infinite_primes
using the set.infinite
predicate.
Equations
- nat.primes.has_repr = {repr := λ (p : nat.primes), repr p.val}
Equations
Equations
- nat.primes.coe_nat = {coe := subtype.val (λ (p : ℕ), nat.prime p)}
Equations
- nat.monoid.prime_pow = {pow := λ (x : α) (p : nat.primes), x ^ p.val}
Primality prover #
A partial proof of factors
. Asserts that l
is a sorted list of primes, lower bounded by a
prime p
, which multiplies to n
.