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 : Nat.Prime p) (h_two : p ≠ 2) (h_three : p ≠ 3) : 5 ≤ p

theorem Nat.Prime.pred_pos {p : ℕ} (pp : Nat.Prime p) : 0 < p.pred

theorem Nat.succ_pred_prime {p : ℕ} (pp : Nat.Prime p) : p.pred.succ = p

theorem Nat.exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬Nat.Prime n) : ∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n

theorem Nat.exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Nat.Prime n) : ∃ (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) : ¬Nat.Prime n

theorem Nat.not_prime_of_dvd_of_lt {m : ℕ} {n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) : ¬Nat.Prime n

theorem Nat.not_prime_iff_exists_dvd_ne {n : ℕ} (h : 2 ≤ n) : ¬Nat.Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n

theorem Nat.not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) : ¬Nat.Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n

theorem Nat.dvd_of_forall_prime_mul_dvd {a : ℕ} {b : ℕ} (hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ a → p * a ∣ b) : a ∣ b

theorem Nat.exists_infinite_primes (n : ℕ) : ∃ (p : ℕ), n ≤ p ∧ Nat.Prime p

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

theorem Nat.not_bddAbove_setOf_prime : ¬BddAbove {p : ℕ | Nat.Prime p}

A version of Nat.exists_infinite_primes using the BddAbove predicate.

theorem Nat.Prime.eq_two_or_odd {p : ℕ} (hp : Nat.Prime p) : p = 2 ∨ p % 2 = 1

theorem Nat.Prime.eq_two_or_odd' {p : ℕ} (hp : Nat.Prime p) : p = 2 ∨ Odd p

theorem Nat.Prime.even_iff {p : ℕ} (hp : Nat.Prime p) : Even p ↔ p = 2

theorem Nat.Prime.odd_of_ne_two {p : ℕ} (hp : Nat.Prime p) (h_two : p ≠ 2) : Odd p

theorem Nat.Prime.even_sub_one {p : ℕ} (hp : Nat.Prime p) (h2 : p ≠ 2) : Even (p - 1)

theorem Nat.Prime.mod_two_eq_one_iff_ne_two {p : ℕ} [Fact (Nat.Prime p)] : 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 : ℕ), Nat.Prime k → k ∣ m → k ∣ n → k ∣ 1) : m.Coprime n

theorem Nat.factors_lemma {k : ℕ} : (k + 2) / (k + 2).minFac < k + 2

theorem Nat.Prime.dvd_iff_not_coprime {p : ℕ} {n : ℕ} (pp : Nat.Prime p) : p ∣ n ↔ ¬p.Coprime n

theorem Nat.Prime.not_coprime_iff_dvd {m : ℕ} {n : ℕ} : ¬m.Coprime n ↔ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p ∣ n

theorem Nat.Prime.not_dvd_mul {p : ℕ} {m : ℕ} {n : ℕ} (pp : Nat.Prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) : ¬p ∣ m * n

@[simp]

theorem Nat.coprime_two_left {n : ℕ} : Nat.Coprime 2 n ↔ Odd n

@[simp]

theorem Nat.coprime_two_right {n : ℕ} : n.Coprime 2 ↔ Odd n

theorem Nat.Coprime.odd_of_left {n : ℕ} : Nat.Coprime 2 n → Odd n

Alias of the forward direction of Nat.coprime_two_left.

theorem Odd.coprime_two_left {n : ℕ} : Odd n → Nat.Coprime 2 n

Alias of the reverse direction of Nat.coprime_two_left.

theorem Odd.coprime_two_right {n : ℕ} : Odd n → n.Coprime 2

Alias of the reverse direction of Nat.coprime_two_right.

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

Alias of the forward direction of Nat.coprime_two_right.

theorem Nat.irreducible_iff_prime {p : ℕ} : Irreducible p ↔ Prime p

theorem Nat.Prime.dvd_of_dvd_pow {p : ℕ} {m : ℕ} {n : ℕ} (pp : Nat.Prime p) (h : p ∣ m ^ n) : p ∣ m

theorem Nat.Prime.not_prime_pow' {x : ℕ} {n : ℕ} (hn : n ≠ 1) : ¬Nat.Prime (x ^ n)

theorem Nat.Prime.not_prime_pow {x : ℕ} {n : ℕ} (hn : 2 ≤ n) : ¬Nat.Prime (x ^ 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 : Nat.Prime p) : 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 : Nat.Prime p) (hk : k ≠ 0) : (p ^ k).minFac = p

theorem Nat.Prime.mul_eq_prime_sq_iff {x : ℕ} {y : ℕ} {p : ℕ} (hp : Nat.Prime p) (hx : x ≠ 1) (hy : y ≠ 1) : x * y = p ^ 2 ↔ x = p ∧ y = p

theorem Nat.Prime.dvd_factorial {n : ℕ} {p : ℕ} : Nat.Prime p → (p ∣ n.factorial ↔ p ≤ n)

theorem Nat.Prime.coprime_pow_of_not_dvd {p : ℕ} {m : ℕ} {a : ℕ} (pp : Nat.Prime p) (h : ¬p ∣ a) : a.Coprime (p ^ m)

theorem Nat.coprime_primes {p : ℕ} {q : ℕ} (pp : Nat.Prime p) (pq : Nat.Prime q) : p.Coprime q ↔ p ≠ q

theorem Nat.coprime_pow_primes {p : ℕ} {q : ℕ} (n : ℕ) (m : ℕ) (pp : Nat.Prime p) (pq : Nat.Prime q) (h : p ≠ q) : (p ^ n).Coprime (q ^ m)

theorem Nat.coprime_or_dvd_of_prime {p : ℕ} (pp : Nat.Prime p) (i : ℕ) : p.Coprime i ∨ p ∣ i

theorem Nat.coprime_of_lt_prime {n : ℕ} {p : ℕ} (n_pos : 0 < n) (hlt : n < p) (pp : Nat.Prime p) : p.Coprime n

theorem Nat.eq_or_coprime_of_le_prime {n : ℕ} {p : ℕ} (n_pos : 0 < n) (hle : n ≤ p) (pp : Nat.Prime p) : p = n ∨ p.Coprime n

theorem Nat.dvd_prime_pow {p : ℕ} (pp : Nat.Prime p) {m : ℕ} {i : ℕ} : i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k

theorem Nat.Prime.dvd_mul_of_dvd_ne {p1 : ℕ} {p2 : ℕ} {n : ℕ} (h_neq : p1 ≠ p2) (pp1 : Nat.Prime p1) (pp2 : Nat.Prime p2) (h1 : p1 ∣ n) (h2 : p2 ∣ n) : p1 * p2 ∣ n

theorem Nat.eq_prime_pow_of_dvd_least_prime_pow {a : ℕ} {p : ℕ} {k : ℕ} (pp : Nat.Prime p) (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 : ℕ), Nat.Prime p ∧ p ∣ n

theorem Nat.eq_one_iff_not_exists_prime_dvd {n : ℕ} : n = 1 ↔ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ n

theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : Nat.Prime p) {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 : ℕ} : Nat.Prime p ↔ Prime ↑p

theorem Nat.Prime.pow_inj {p : ℕ} {q : ℕ} {m : ℕ} {n : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (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, ∀ n ≥ n0, c ^ n < (n - 1).factorial

theorem Nat.exists_mul_pow_lt_factorial (a : ℕ) (c : ℕ) : ∃ (n0 : ℕ), ∀ n ≥ n0, a * c ^ n < (n - 1).factorial

theorem Nat.exists_prime_mul_pow_lt_factorial (n : ℕ) (a : ℕ) (c : ℕ) : ∃ p > n, Nat.Prime p ∧ a * c ^ p < (p - 1).factorial

theorem Int.prime_two : Prime 2

theorem Int.prime_three : Prime 3