# Documentation

## Notable Theorems #

• 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).
theorem Nat.Prime.five_le_of_ne_two_of_ne_three {p : } (hp : ) (h_two : p 2) (h_three : p 3) :
5 p
theorem Nat.Prime.pred_pos {p : } (pp : ) :
0 < p.pred
theorem Nat.succ_pred_prime {p : } (pp : ) :
p.pred.succ = p
theorem Nat.exists_dvd_of_not_prime {n : } (n2 : 2 n) (np : ) :
∃ (m : ), m n m 1 m n
theorem Nat.exists_dvd_of_not_prime2 {n : } (n2 : 2 n) (np : ) :
∃ (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) :
theorem Nat.not_prime_of_dvd_of_lt {m : } {n : } (h1 : m n) (h2 : 2 m) (h3 : m < n) :
theorem Nat.not_prime_iff_exists_dvd_ne {n : } (h : 2 n) :
∃ (m : ), m n m 1 m n
theorem Nat.not_prime_iff_exists_dvd_lt {n : } (h : 2 n) :
∃ (m : ), m n 2 m m < n
theorem Nat.dvd_of_forall_prime_mul_dvd {a : } {b : } (hdvd : ∀ (p : ), p ap * a b) :
a b
theorem Nat.exists_infinite_primes (n : ) :
∃ (p : ), n p

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.even_iff {p : } (hp : ) :
Even p p = 2
theorem Nat.Prime.odd_of_ne_two {p : } (hp : ) (h_two : p 2) :
Odd p
theorem Nat.Prime.even_sub_one {p : } (hp : ) (h2 : p 2) :
Even (p - 1)
theorem Nat.Prime.mod_two_eq_one_iff_ne_two {p : } [Fact ()] :
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 mk nk 1) :
m.Coprime n
theorem Nat.Prime.dvd_iff_not_coprime {p : } {n : } (pp : ) :
p n ¬p.Coprime n
theorem Nat.Prime.not_coprime_iff_dvd {m : } {n : } :
¬m.Coprime n ∃ (p : ), p m p n
theorem Nat.Prime.not_dvd_mul {p : } {m : } {n : } (pp : ) (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 Nat.Coprime.odd_of_right {n : } :
n.Coprime 2Odd n

Alias of the forward direction of Nat.coprime_two_right.

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

Alias of the reverse direction of Nat.coprime_two_right.

theorem Nat.Prime.dvd_of_dvd_pow {p : } {m : } {n : } (pp : ) (h : p m ^ n) :
p m
theorem Nat.Prime.not_prime_pow' {x : } {n : } (hn : n 1) :
theorem Nat.Prime.not_prime_pow {x : } {n : } (hn : 2 n) :
theorem Nat.Prime.eq_one_of_pow {x : } {n : } (h : Nat.Prime (x ^ n)) :
n = 1
theorem Nat.Prime.pow_eq_iff {p : } {a : } {k : } (hp : ) :
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 : ) (hk : k 0) :
(p ^ k).minFac = p
theorem Nat.Prime.mul_eq_prime_sq_iff {x : } {y : } {p : } (hp : ) (hx : x 1) (hy : y 1) :
x * y = p ^ 2 x = p y = p
theorem Nat.Prime.dvd_factorial {n : } {p : } :
(p n.factorial p n)
theorem Nat.Prime.coprime_pow_of_not_dvd {p : } {m : } {a : } (pp : ) (h : ¬p a) :
a.Coprime (p ^ m)
theorem Nat.coprime_primes {p : } {q : } (pp : ) (pq : ) :
p.Coprime q p q
theorem Nat.coprime_pow_primes {p : } {q : } (n : ) (m : ) (pp : ) (pq : ) (h : p q) :
(p ^ n).Coprime (q ^ m)
theorem Nat.coprime_or_dvd_of_prime {p : } (pp : ) (i : ) :
p.Coprime i p i
theorem Nat.coprime_of_lt_prime {n : } {p : } (n_pos : 0 < n) (hlt : n < p) (pp : ) :
p.Coprime n
theorem Nat.eq_or_coprime_of_le_prime {n : } {p : } (n_pos : 0 < n) (hle : n p) (pp : ) :
p = n p.Coprime n
theorem Nat.dvd_prime_pow {p : } (pp : ) {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 : ) (pp2 : ) (h1 : p1 n) (h2 : p2 n) :
p1 * p2 n
theorem Nat.eq_prime_pow_of_dvd_least_prime_pow {a : } {p : } {k : } (pp : ) (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 n
theorem Nat.eq_one_iff_not_exists_prime_dvd {n : } :
n = 1 ∀ (p : ), ¬p n
theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : } (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.pow_inj {p : } {q : } {m : } {n : } (hp : ) (hq : ) (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, a * c ^ p < (p - 1).factorial