Prime numbers
This file deals with prime numbers: natural numbers p ≥ 2 whose only divisors are p and 1.
Important declarations
All the following declarations exist in the namespace nat.
prime: the predicate that expresses that a natural numberpis primeprimes: the subtype of natural numbers that are primemin_fac n: the minimal prime factor of a natural numbern ≠ 1exists_infinite_primes: Euclid's theorem that there exist infinitely many prime numbersfactors n: the prime factorization ofnfactors_unique: uniqueness of the prime factorisation
This instance is slower than the instance decidable_prime defined below,
but has the advantage that it works 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_1 = decidable_of_iff' (2 ≤ p ∧ ∀ (m : ℕ), 2 ≤ m → m < p → ¬m ∣ p) nat.prime_def_lt'
Equations
- n.min_fac_aux k = ite (n < k * k) n (ite (k ∣ n) k (n.min_fac_aux (k + 2)))
@[instance]
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
@[instance]
Equations
- nat.primes.has_repr = {repr := λ (p : nat.primes), repr p.val}
@[instance]
Equations
- nat.primes.inhabited = {default := ⟨2, nat.prime_two⟩}
@[instance]
Equations
- nat.primes.coe_nat = {coe := subtype.val (λ (p : ℕ), nat.prime p)}
@[instance]
Equations
- nat.monoid.prime_pow = {pow := λ (x : α) (p : nat.primes), x ^ p.val}