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.exists_infinite_primes
: Euclid's theorem that there exist infinitely many prime numbers. This also appears asNat.not_bddAbove_setOf_prime
andNat.infinite_setOf_prime
(the latter inData.Nat.PrimeFin
).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
This instance is slower than the instance decidablePrime
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 by decide
, but rather by norm_num
, which is
much faster.
Equations
- Nat.decidablePrime1 p = decidable_of_iff' (2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p) ⋯
Instances For
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
.
Equations
- Nat.minFacAux n x = if h : n < x * x then n else if x ∣ n then x else let_fun this := ⋯; Nat.minFacAux n (x + 2)
Instances For
Returns the smallest prime factor of n ≠ 1
.
Equations
- Nat.minFac n = if 2 ∣ n then 2 else Nat.minFacAux n 3
Instances For
This instance is faster in the virtual machine than decidablePrime1
,
but slower in the kernel.
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
- Nat.decidablePrime p = decidable_of_iff' (2 ≤ p ∧ Nat.minFac p = p) ⋯
The square of the smallest prime factor of a composite number n
is at most n
.
A version of Nat.exists_infinite_primes
using the BddAbove
predicate.
Alias of the reverse direction of Nat.coprime_two_left
.
Alias of the forward direction of Nat.coprime_two_left
.
Alias of the reverse direction of Nat.coprime_two_right
.
Alias of the forward direction of Nat.coprime_two_right
.
Alias of the forward direction of Nat.prime_iff
.
Alias of the reverse direction of Nat.prime_iff
.
Equations
- Nat.Primes.instReprPrimes = { reprPrec := fun (p : Nat.Primes) (x : ℕ) => repr ↑p }
Equations
- Nat.Primes.inhabitedPrimes = { default := { val := 2, property := Nat.prime_two } }
Equations
- Nat.Primes.coeNat = { coe := Subtype.val }
Equations
- Nat.monoid.primePow = { pow := fun (x : α) (p : Nat.Primes) => x ^ ↑p }