# 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 number p is prime
• Nat.Primes: the subtype of natural numbers that are prime
• Nat.minFac n: the minimal prime factor of a natural number n ≠ 1
• Nat.prime_iff: Nat.Prime coincides with the general definition of Prime
• Nat.irreducible_iff_nat_prime: a non-unit natural number is only divisible by 1 iff it is prime
def Nat.Prime (p : ) :

Nat.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
Instances For
theorem Nat.Prime.ne_zero {n : } (h : ) :
n 0
theorem Nat.Prime.pos {p : } (pp : ) :
0 < p
theorem Nat.Prime.two_le {p : } :
2 p
theorem Nat.Prime.one_lt {p : } :
1 < p
theorem Nat.Prime.one_le {p : } (hp : ) :
1 p
instance Nat.Prime.one_lt' (p : ) [hp : Fact (Nat.Prime p)] :
Fact (1 < p)
Equations
• =
theorem Nat.Prime.ne_one {p : } (hp : ) :
p 1
theorem Nat.Prime.eq_one_or_self_of_dvd {p : } (pp : ) (m : ) (hm : m p) :
m = 1 m = p
theorem Nat.prime_def_lt'' {p : } :
2 p ∀ (m : ), m pm = 1 m = p
theorem Nat.prime_def_lt {p : } :
2 p ∀ (m : ), m < pm pm = 1
theorem Nat.prime_def_lt' {p : } :
2 p ∀ (m : ), 2 mm < p¬m p
theorem Nat.prime_def_le_sqrt {p : } :
2 p ∀ (m : ), 2 mm p.sqrt¬m p
theorem Nat.prime_of_coprime (n : ) (h1 : 1 < n) (h : ∀ (m : ), m < nm 0n.Coprime m) :

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
Instances For
theorem Nat.dvd_prime {p : } {m : } (pp : ) :
m p m = 1 m = p
theorem Nat.dvd_prime_two_le {p : } {m : } (pp : ) (H : 2 m) :
m p m = p
theorem Nat.prime_dvd_prime_iff_eq {p : } {q : } (pp : ) (qp : ) :
p q p = q
theorem Nat.Prime.not_dvd_one {p : } (pp : ) :
¬p 1
theorem Nat.prime_mul_iff {a : } {b : } :
Nat.Prime (a * b) b = 1 a = 1
theorem Nat.not_prime_mul {a : } {b : } (a1 : a 1) (b1 : b 1) :
theorem Nat.not_prime_mul' {a : } {b : } {n : } (h : a * b = n) (h₁ : a 1) (h₂ : b 1) :
theorem Nat.Prime.dvd_iff_eq {p : } {a : } (hp : ) (a1 : a 1) :
a p p = a
theorem Nat.Prime.eq_two_or_odd {p : } (hp : ) :
p = 2 p % 2 = 1
theorem Nat.Prime.eq_two_or_odd' {p : } (hp : ) :
p = 2 Odd p
theorem Nat.minFac_lemma (n : ) (k : ) (h : ¬n < k * k) :
n.sqrt - k < n.sqrt + 2 - k
def Nat.minFacAux (n : ) :

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
• n.minFacAux x = if n < x * x then n else if x n then x else n.minFacAux (x + 2)
Instances For
def Nat.minFac (n : ) :

Returns the smallest prime factor of n ≠ 1.

Equations
• n.minFac = if 2 n then 2 else n.minFacAux 3
Instances For
@[simp]
theorem Nat.minFac_zero :
= 2
@[simp]
theorem Nat.minFac_one :
= 1
@[simp]
theorem Nat.minFac_two :
= 2
theorem Nat.minFac_eq (n : ) :
n.minFac = if 2 n then 2 else n.minFacAux 3
@[irreducible]
theorem Nat.minFacAux_has_prop {n : } (n2 : 2 n) (k : ) (i : ) :
k = 2 * i + 3(∀ (m : ), 2 mm nk m)Nat.minFacProp n (n.minFacAux k)
theorem Nat.minFac_has_prop {n : } (n1 : n 1) :
Nat.minFacProp n n.minFac
theorem Nat.minFac_dvd (n : ) :
n.minFac n
theorem Nat.minFac_prime {n : } (n1 : n 1) :
Nat.Prime n.minFac
theorem Nat.minFac_le_of_dvd {n : } {m : } :
2 mm nn.minFac m
theorem Nat.minFac_pos (n : ) :
0 < n.minFac
theorem Nat.minFac_le {n : } (H : 0 < n) :
n.minFac n
theorem Nat.le_minFac {m : } {n : } :
n = 1 m n.minFac ∀ (p : ), p nm p
theorem Nat.le_minFac' {m : } {n : } :
n = 1 m n.minFac ∀ (p : ), 2 pp nm p
theorem Nat.prime_def_minFac {p : } :
2 p p.minFac = p
@[simp]
theorem Nat.Prime.minFac_eq {p : } (hp : ) :
p.minFac = p
instance Nat.decidablePrime (p : ) :

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
theorem Nat.not_prime_iff_minFac_lt {n : } (n2 : 2 n) :
n.minFac < n
theorem Nat.minFac_le_div {n : } (pos : 0 < n) (np : ) :
n.minFac n / n.minFac
theorem Nat.minFac_sq_le_self {n : } (w : 0 < n) (h : ) :
n.minFac ^ 2 n

The square of the smallest prime factor of a composite number n is at most n.

@[simp]
theorem Nat.minFac_eq_one_iff {n : } :
n.minFac = 1 n = 1
@[simp]
theorem Nat.minFac_eq_two_iff (n : ) :
n.minFac = 2 2 n
theorem Nat.factors_lemma {k : } :
(k + 2) / (k + 2).minFac < k + 2
theorem Nat.exists_prime_and_dvd {n : } (hn : n 1) :
∃ (p : ), p n
theorem Nat.coprime_of_dvd {m : } {n : } (H : ∀ (k : ), k m¬k n) :
m.Coprime n
theorem Nat.Prime.coprime_iff_not_dvd {p : } {n : } (pp : ) :
p.Coprime n ¬p n
theorem Nat.Prime.dvd_mul {p : } {m : } {n : } (pp : ) :
p m * n p m p n
theorem Nat.prime_iff {p : } :
theorem Prime.nat_prime {p : } :

Alias of the reverse direction of Nat.prime_iff.

theorem Nat.Prime.prime {p : } :

Alias of the forward direction of Nat.prime_iff.

The type of prime numbers

Equations
Instances For
Equations
Equations
Equations
theorem Nat.Primes.coe_nat_inj (p : Nat.Primes) (q : Nat.Primes) :
p = q p = q
instance Nat.monoid.primePow {α : Type u_1} [] :
Equations
• Nat.monoid.primePow = { pow := fun (x : α) (p : Nat.Primes) => x ^ p }
Equations