# 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.exists_infinite_primes: Euclid's theorem that there exist infinitely many prime numbers. This also appears as Nat.not_bddAbove_setOf_prime and Nat.infinite_setOf_prime (the latter in Data.Nat.PrimeFin).
• 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
• p.Prime =
Instances For
theorem Nat.Prime.ne_zero {n : } (h : n.Prime) :
n 0
theorem Nat.Prime.pos {p : } (pp : p.Prime) :
0 < p
theorem Nat.Prime.two_le {p : } :
p.Prime2 p
theorem Nat.Prime.one_lt {p : } :
p.Prime1 < p
theorem Nat.Prime.one_le {p : } (hp : p.Prime) :
1 p
instance Nat.Prime.one_lt' (p : ) [hp : Fact p.Prime] :
Fact (1 < p)
Equations
• =
theorem Nat.Prime.ne_one {p : } (hp : p.Prime) :
p 1
theorem Nat.Prime.eq_one_or_self_of_dvd {p : } (pp : p.Prime) (m : ) (hm : m p) :
m = 1 m = p
theorem Nat.prime_def_lt'' {p : } :
p.Prime 2 p ∀ (m : ), m pm = 1 m = p
theorem Nat.prime_def_lt {p : } :
p.Prime 2 p m < p, m pm = 1
theorem Nat.prime_def_lt' {p : } :
p.Prime 2 p ∀ (m : ), 2 mm < p¬m p
theorem Nat.prime_def_le_sqrt {p : } :
p.Prime 2 p ∀ (m : ), 2 mm p.sqrt¬m p
theorem Nat.prime_of_coprime (n : ) (h1 : 1 < n) (h : m < n, m 0n.Coprime m) :
n.Prime
def Nat.decidablePrime1 (p : ) :
Decidable p.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
Instances For
theorem Nat.Prime.five_le_of_ne_two_of_ne_three {p : } (hp : p.Prime) (h_two : p 2) (h_three : p 3) :
5 p
theorem Nat.Prime.pred_pos {p : } (pp : p.Prime) :
0 < p.pred
theorem Nat.succ_pred_prime {p : } (pp : p.Prime) :
p.pred.succ = p
theorem Nat.dvd_prime {p : } {m : } (pp : p.Prime) :
m p m = 1 m = p
theorem Nat.dvd_prime_two_le {p : } {m : } (pp : p.Prime) (H : 2 m) :
m p m = p
theorem Nat.prime_dvd_prime_iff_eq {p : } {q : } (pp : p.Prime) (qp : q.Prime) :
p q p = q
theorem Nat.Prime.not_dvd_one {p : } (pp : p.Prime) :
¬p 1
theorem Nat.prime_mul_iff {a : } {b : } :
(a * b).Prime a.Prime b = 1 b.Prime a = 1
theorem Nat.not_prime_mul {a : } {b : } (a1 : a 1) (b1 : b 1) :
¬(a * b).Prime
theorem Nat.not_prime_mul' {a : } {b : } {n : } (h : a * b = n) (h₁ : a 1) (h₂ : b 1) :
¬n.Prime
theorem Nat.Prime.dvd_iff_eq {p : } {a : } (hp : p.Prime) (a1 : a 1) :
a p p = a
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) :
n.minFac.Prime
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.Primep nm p
theorem Nat.le_minFac' {m : } {n : } :
n = 1 m n.minFac ∀ (p : ), 2 pp nm p
theorem Nat.prime_def_minFac {p : } :
p.Prime 2 p p.minFac = p
@[simp]
theorem Nat.Prime.minFac_eq {p : } (hp : p.Prime) :
p.minFac = p
instance Nat.decidablePrime (p : ) :
Decidable p.Prime

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.Prime n.minFac < n
theorem Nat.minFac_le_div {n : } (pos : 0 < n) (np : ¬n.Prime) :
n.minFac n / n.minFac
theorem Nat.minFac_sq_le_self {n : } (w : 0 < n) (h : ¬n.Prime) :
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.exists_dvd_of_not_prime {n : } (n2 : 2 n) (np : ¬n.Prime) :
∃ (m : ), m n m 1 m n
theorem Nat.exists_dvd_of_not_prime2 {n : } (n2 : 2 n) (np : ¬n.Prime) :
∃ (m : ), m n 2 m m < n
theorem Nat.not_prime_of_dvd_of_ne {m : } {n : } (h1 : m n) (h2 : m 1) (h3 : m n) :
¬n.Prime
theorem Nat.not_prime_of_dvd_of_lt {m : } {n : } (h1 : m n) (h2 : 2 m) (h3 : m < n) :
¬n.Prime
theorem Nat.not_prime_iff_exists_dvd_ne {n : } (h : 2 n) :
¬n.Prime ∃ (m : ), m n m 1 m n
theorem Nat.not_prime_iff_exists_dvd_lt {n : } (h : 2 n) :
¬n.Prime ∃ (m : ), m n 2 m m < n
theorem Nat.exists_prime_and_dvd {n : } (hn : n 1) :
∃ (p : ), p.Prime p n
theorem Nat.dvd_of_forall_prime_mul_dvd {a : } {b : } (hdvd : ∀ (p : ), p.Primep ap * a b) :
a b
theorem Nat.exists_infinite_primes (n : ) :
∃ (p : ), n p p.Prime

Euclid's theorem on the infinitude of primes. Here given in the form: for every n, there exists a prime number p ≥ n.

A version of Nat.exists_infinite_primes using the BddAbove predicate.

theorem Nat.Prime.eq_two_or_odd {p : } (hp : p.Prime) :
p = 2 p % 2 = 1
theorem Nat.Prime.eq_two_or_odd' {p : } (hp : p.Prime) :
p = 2 Odd p
theorem Nat.Prime.even_iff {p : } (hp : p.Prime) :
Even p p = 2
theorem Nat.Prime.odd_of_ne_two {p : } (hp : p.Prime) (h_two : p 2) :
Odd p
theorem Nat.Prime.even_sub_one {p : } (hp : p.Prime) (h2 : p 2) :
Even (p - 1)
theorem Nat.Prime.mod_two_eq_one_iff_ne_two {p : } [Fact p.Prime] :
p % 2 = 1 p 2

A prime p satisfies p % 2 = 1 if and only if p ≠ 2.

theorem Nat.coprime_of_dvd {m : } {n : } (H : ∀ (k : ), k.Primek m¬k n) :
m.Coprime n
theorem Nat.coprime_of_dvd' {m : } {n : } (H : ∀ (k : ), k.Primek mk nk 1) :
m.Coprime n
theorem Nat.factors_lemma {k : } :
(k + 2) / (k + 2).minFac < k + 2
theorem Nat.Prime.coprime_iff_not_dvd {p : } {n : } (pp : p.Prime) :
p.Coprime n ¬p n
theorem Nat.Prime.dvd_iff_not_coprime {p : } {n : } (pp : p.Prime) :
p n ¬p.Coprime n
theorem Nat.Prime.not_coprime_iff_dvd {m : } {n : } :
¬m.Coprime n ∃ (p : ), p.Prime p m p n
theorem Nat.Prime.dvd_mul {p : } {m : } {n : } (pp : p.Prime) :
p m * n p m p n
theorem Nat.Prime.not_dvd_mul {p : } {m : } {n : } (pp : p.Prime) (Hm : ¬p m) (Hn : ¬p n) :
¬p m * n
@[simp]
theorem Nat.coprime_two_left {n : } :
Odd n
@[simp]
theorem Nat.coprime_two_right {n : } :
n.Coprime 2 Odd n
theorem Nat.Coprime.odd_of_left {n : } :
Odd n

Alias of the forward direction of Nat.coprime_two_left.

theorem Odd.coprime_two_left {n : } :
Odd n

Alias of the reverse direction of Nat.coprime_two_left.

theorem Odd.coprime_two_right {n : } :
Odd nn.Coprime 2

Alias of the reverse direction of Nat.coprime_two_right.

theorem Nat.Coprime.odd_of_right {n : } :
n.Coprime 2Odd n

Alias of the forward direction of Nat.coprime_two_right.

theorem Nat.prime_iff {p : } :
p.Prime
theorem Nat.Prime.prime {p : } :
p.Prime

Alias of the forward direction of Nat.prime_iff.

theorem Prime.nat_prime {p : } :
p.Prime

Alias of the reverse direction of Nat.prime_iff.

theorem Nat.Prime.dvd_of_dvd_pow {p : } {m : } {n : } (pp : p.Prime) (h : p m ^ n) :
p m
theorem Nat.Prime.not_prime_pow' {x : } {n : } (hn : n 1) :
¬(x ^ n).Prime
theorem Nat.Prime.not_prime_pow {x : } {n : } (hn : 2 n) :
¬(x ^ n).Prime
theorem Nat.Prime.eq_one_of_pow {x : } {n : } (h : (x ^ n).Prime) :
n = 1
theorem Nat.Prime.pow_eq_iff {p : } {a : } {k : } (hp : p.Prime) :
a ^ k = p a = p k = 1
theorem Nat.pow_minFac {n : } {k : } (hk : k 0) :
(n ^ k).minFac = n.minFac
theorem Nat.Prime.pow_minFac {p : } {k : } (hp : p.Prime) (hk : k 0) :
(p ^ k).minFac = p
theorem Nat.Prime.mul_eq_prime_sq_iff {x : } {y : } {p : } (hp : p.Prime) (hx : x 1) (hy : y 1) :
x * y = p ^ 2 x = p y = p
theorem Nat.Prime.dvd_factorial {n : } {p : } :
p.Prime(p n.factorial p n)
theorem Nat.Prime.coprime_pow_of_not_dvd {p : } {m : } {a : } (pp : p.Prime) (h : ¬p a) :
a.Coprime (p ^ m)
theorem Nat.coprime_primes {p : } {q : } (pp : p.Prime) (pq : q.Prime) :
p.Coprime q p q
theorem Nat.coprime_pow_primes {p : } {q : } (n : ) (m : ) (pp : p.Prime) (pq : q.Prime) (h : p q) :
(p ^ n).Coprime (q ^ m)
theorem Nat.coprime_or_dvd_of_prime {p : } (pp : p.Prime) (i : ) :
p.Coprime i p i
theorem Nat.coprime_of_lt_prime {n : } {p : } (n_pos : 0 < n) (hlt : n < p) (pp : p.Prime) :
p.Coprime n
theorem Nat.eq_or_coprime_of_le_prime {n : } {p : } (n_pos : 0 < n) (hle : n p) (pp : p.Prime) :
p = n p.Coprime n
theorem Nat.dvd_prime_pow {p : } (pp : p.Prime) {m : } {i : } :
i p ^ m km, i = p ^ k
theorem Nat.Prime.dvd_mul_of_dvd_ne {p1 : } {p2 : } {n : } (h_neq : p1 p2) (pp1 : p1.Prime) (pp2 : p2.Prime) (h1 : p1 n) (h2 : p2 n) :
p1 * p2 n
theorem Nat.eq_prime_pow_of_dvd_least_prime_pow {a : } {p : } {k : } (pp : p.Prime) (h₁ : ¬a p ^ k) (h₂ : a p ^ (k + 1)) :
a = p ^ (k + 1)

If p is prime, and a doesn't divide p^k, but a does divide p^(k+1) then a = p^(k+1).

theorem Nat.ne_one_iff_exists_prime_dvd {n : } :
n 1 ∃ (p : ), p.Prime p n
theorem Nat.eq_one_iff_not_exists_prime_dvd {n : } :
n = 1 ∀ (p : ), p.Prime¬p n
theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : } (p_prime : p.Prime) {m : } {n : } {k : } {l : } (hpm : p ^ k m) (hpn : p ^ l n) (hpmn : p ^ (k + l + 1) m * n) :
p ^ (k + 1) m p ^ (l + 1) n
theorem Nat.prime_iff_prime_int {p : } :
p.Prime Prime p
theorem Nat.Prime.pow_inj {p : } {q : } {m : } {n : } (hp : p.Prime) (hq : q.Prime) (h : p ^ (m + 1) = q ^ (n + 1)) :
p = q m = n

Two prime powers with positive exponents are equal only when the primes and the exponents are equal.

theorem Nat.exists_pow_lt_factorial (c : ) :
n0 > 1, nn0, c ^ n < (n - 1).factorial
theorem Nat.exists_mul_pow_lt_factorial (a : ) (c : ) :
∃ (n0 : ), nn0, a * c ^ n < (n - 1).factorial
theorem Nat.exists_prime_mul_pow_lt_factorial (n : ) (a : ) (c : ) :
p > n, p.Prime a * c ^ p < (p - 1).factorial

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
Equations