# Prime numbers #

This file develops the theory of prime numbers: natural numbers `p ≥ 2` whose only divisors are `p` and `1`.

source
theorem Nat.prime_mul_iff {a b : ℕ} :
Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1
source
theorem Nat.not_prime_mul {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) :
¬Prime (a * b)
source
theorem Nat.not_prime_of_mul_eq {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) :
¬Prime n
source
@[deprecated Nat.not_prime_of_mul_eq (since := "2025-05-24")]
theorem Nat.not_prime_mul' {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) :
¬Prime n

Alias of `Nat.not_prime_of_mul_eq`.

source
theorem Nat.Prime.dvd_iff_eq {p a : ℕ} (hp : Prime p) (a1 : a ≠ 1) :
a ∣ p ↔ p = a
source
theorem Nat.Prime.eq_two_or_odd {p : ℕ} (hp : Prime p) :
p = 2 ∨ p % 2 = 1
source
theorem Nat.Prime.eq_two_or_odd' {p : ℕ} (hp : Prime p) :
p = 2 ∨ Odd p
source
theorem Nat.Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : Prime p) (h_two : p ≠ 2) (h_three : p ≠ 3) :
5 ≤ p
source
theorem Nat.Prime.pred_pos {p : ℕ} (pp : Prime p) :
0 < p.pred
source
theorem Nat.succ_pred_prime {p : ℕ} (pp : Prime p) :
p.pred.succ = p
source
theorem Nat.exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) :
∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n
source
theorem Nat.exists_dvd_of_not_prime2 {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) :
∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n
source
theorem Nat.not_prime_of_dvd_of_ne {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) :
¬Prime n
source
theorem Nat.not_prime_of_dvd_of_lt {m n : ℕ} (h1 : m ∣ n) (h2 : 2 ≤ m) (h3 : m < n) :
¬Prime n
source
theorem Nat.not_prime_iff_exists_dvd_ne {n : ℕ} (h : 2 ≤ n) :
¬Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ m ≠ 1 ∧ m ≠ n
source
theorem Nat.not_prime_iff_exists_dvd_lt {n : ℕ} (h : 2 ≤ n) :
¬Prime n ↔ ∃ (m : ℕ), m ∣ n ∧ 2 ≤ m ∧ m < n
source
theorem Nat.not_prime_iff_exists_mul_eq {n : ℕ} (h : 2 ≤ n) :
¬Prime n ↔ ∃ (a : ℕ), ∃ (b : ℕ), a < n ∧ b < n ∧ a * b = n
source
theorem Nat.dvd_of_forall_prime_mul_dvd {a b : ℕ} (hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b) :
a ∣ b
source
theorem Nat.Prime.even_iff {p : ℕ} (hp : Prime p) :
Even p ↔ p = 2
source
theorem Nat.Prime.odd_of_ne_two {p : ℕ} (hp : Prime p) (h_two : p ≠ 2) :
Odd p
source
theorem Nat.Prime.even_sub_one {p : ℕ} (hp : Prime p) (h2 : p ≠ 2) :
Even (p - 1)
source
theorem Nat.Prime.mod_two_eq_one_iff_ne_two {p : ℕ} (hp : Prime p) :
p % 2 = 1 ↔ p ≠ 2

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

source
theorem Nat.coprime_of_dvd' {m n : ℕ} (H : ∀ (k : ℕ), Prime k → k ∣ m → k ∣ n → k ∣ 1) :
m.Coprime n
source
theorem Nat.Prime.dvd_iff_not_coprime {p n : ℕ} (pp : Prime p) :
p ∣ n ↔ ¬p.Coprime n
source
theorem Nat.Prime.not_coprime_iff_dvd {m n : ℕ} :
¬m.Coprime n ↔ ∃ (p : ℕ), Prime p ∧ p ∣ m ∧ p ∣ n
source
theorem Nat.coprime_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < n.minFac) :
n.Coprime m

If `0 < m < minFac n`, then `n` and `m` are coprime.

source
theorem Nat.gcd_eq_one_of_lt_minFac {n m : ℕ} (h₀ : m ≠ 0) (h : m < n.minFac) :
n.gcd m = 1

If `0 < m < minFac n`, then `n` and `m` have gcd equal to `1`.

source
theorem Nat.Prime.not_dvd_mul {p m n : ℕ} (pp : Prime p) (Hm : ¬p ∣ m) (Hn : ¬p ∣ n) :
¬p ∣ m * n
source
@[simp]
theorem Nat.coprime_two_left {n : ℕ} :
Coprime 2 n ↔ Odd n
source
@[simp]
theorem Nat.coprime_two_right {n : ℕ} :
n.Coprime 2 ↔ Odd n
source
theorem Nat.Coprime.odd_of_left {n : ℕ} :
Coprime 2 n → Odd n

Alias of the forward direction of `Nat.coprime_two_left`.

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

Alias of the reverse direction of `Nat.coprime_two_left`.

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

Alias of the forward direction of `Nat.coprime_two_right`.

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

Alias of the reverse direction of `Nat.coprime_two_right`.

source
theorem Nat.Prime.dvd_of_dvd_pow {p m n : ℕ} (pp : Prime p) (h : p ∣ m ^ n) :
p ∣ m
source
theorem Nat.Prime.not_prime_pow' {x n : ℕ} (hn : n ≠ 1) :
¬Prime (x ^ n)
source
theorem Nat.Prime.not_prime_pow {x n : ℕ} (hn : 2 ≤ n) :
¬Prime (x ^ n)
source
theorem Nat.Prime.eq_one_of_pow {x n : ℕ} (h : Prime (x ^ n)) :
n = 1
source
theorem Nat.Prime.pow_eq_iff {p a k : ℕ} (hp : Prime p) :
a ^ k = p ↔ a = p ∧ k = 1
source
theorem Nat.Prime.mul_eq_prime_sq_iff {x y p : ℕ} (hp : Prime p) (hx : x ≠ 1) (hy : y ≠ 1) :
x * y = p ^ 2 ↔ x = p ∧ y = p
source
theorem Nat.Prime.coprime_pow_of_not_dvd {p m a : ℕ} (pp : Prime p) (h : ¬p ∣ a) :
a.Coprime (p ^ m)
source
theorem Nat.coprime_primes {p q : ℕ} (pp : Prime p) (pq : Prime q) :
p.Coprime q ↔ p ≠ q
source
theorem Nat.coprime_pow_primes {p q : ℕ} (n m : ℕ) (pp : Prime p) (pq : Prime q) (h : p ≠ q) :
(p ^ n).Coprime (q ^ m)
source
theorem Nat.coprime_or_dvd_of_prime {p : ℕ} (pp : Prime p) (i : ℕ) :
p.Coprime i ∨ p ∣ i
source
theorem Nat.coprime_of_lt_prime {n p : ℕ} (ne_zero : n ≠ 0) (hlt : n < p) (pp : Prime p) :
p.Coprime n
source
theorem Nat.eq_or_coprime_of_le_prime {n p : ℕ} (ne_zero : n ≠ 0) (hle : n ≤ p) (pp : Prime p) :
p = n ∨ p.Coprime n
source
theorem Nat.prime_eq_prime_of_dvd_pow {m p q : ℕ} (pp : Prime p) (pq : Prime q) (h : p ∣ q ^ m) :
p = q
source
theorem Nat.dvd_prime_pow {p : ℕ} (pp : Prime p) {m i : ℕ} :
i ∣ p ^ m ↔ ∃ (k : ℕ), k ≤ m ∧ i = p ^ k
source
theorem Nat.Prime.dvd_mul_of_dvd_ne {p1 p2 n : ℕ} (h_neq : p1 ≠ p2) (pp1 : Prime p1) (pp2 : Prime p2) (h1 : p1 ∣ n) (h2 : p2 ∣ n) :
p1 * p2 ∣ n
source
theorem Nat.eq_prime_pow_of_dvd_least_prime_pow {a p k : ℕ} (pp : 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)`.

source
theorem Nat.ne_one_iff_exists_prime_dvd {n : ℕ} :
n ≠ 1 ↔ ∃ (p : ℕ), Prime p ∧ p ∣ n
source
theorem Nat.eq_one_iff_not_exists_prime_dvd {n : ℕ} :
n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n
source
theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : 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