Prime numbers

This file deals with the factors of natural numbers.

Important declarations

• Nat.primeFactorsList n: the prime factorization of n
• Nat.primeFactorsList_unique: uniqueness of the prime factorisation

@[irreducible]

def Nat.primeFactorsList : ℕ → List ℕ

primeFactorsList n is the prime factorization of n, listed in increasing order.

Equations

• Nat.primeFactorsList 0 = []
• Nat.primeFactorsList 1 = []
• k.succ.succ.primeFactorsList = (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList

@[simp]

theorem Nat.primeFactorsList_zero : primeFactorsList 0 = []

@[simp]

theorem Nat.primeFactorsList_one : primeFactorsList 1 = []

@[simp]

theorem Nat.primeFactorsList_two : primeFactorsList 2 = [2]

@[irreducible]

theorem Nat.prime_of_mem_primeFactorsList {n p : ℕ} : p ∈ n.primeFactorsList → Prime p

theorem Nat.pos_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ n.primeFactorsList) : 0 < p

@[irreducible]

theorem Nat.prod_primeFactorsList {n : ℕ} : n ≠ 0 → n.primeFactorsList.prod = n

theorem Nat.primeFactorsList_prime {p : ℕ} (hp : Prime p) : p.primeFactorsList = [p]

@[irreducible]

theorem Nat.isChain_cons_primeFactorsList {n a : ℕ} : (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) (a :: n.primeFactorsList)

@[deprecated Nat.isChain_cons_primeFactorsList (since := "2025-09-21")]

theorem Nat.primeFactorsList_chain {n a : ℕ} : (∀ (p : ℕ), Prime p → p ∣ n → a ≤ p) → List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) (a :: n.primeFactorsList)

Alias of Nat.isChain_cons_primeFactorsList.

theorem Nat.isChain_two_cons_primeFactorsList (n : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) (2 :: n.primeFactorsList)

theorem Nat.isChain_primeFactorsList (n : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) n.primeFactorsList

@[deprecated Nat.isChain_two_cons_primeFactorsList (since := "2025-09-24")]

theorem Nat.primeFactorsList_chain_2 (n : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) (2 :: n.primeFactorsList)

Alias of Nat.isChain_two_cons_primeFactorsList.

@[deprecated Nat.isChain_primeFactorsList (since := "2025-09-24")]

theorem Nat.primeFactorsList_chain' (n : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 ≤ x2) n.primeFactorsList

Alias of Nat.isChain_primeFactorsList.

theorem Nat.primeFactorsList_sorted (n : ℕ) : List.Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) n.primeFactorsList

theorem Nat.primeFactorsList_add_two (n : ℕ) : (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList

primeFactorsList can be constructed inductively by extracting minFac, for sufficiently large n.

@[simp]

theorem Nat.primeFactorsList_eq_nil (n : ℕ) : n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

theorem Nat.primeFactorsList_ne_nil (n : ℕ) : n.primeFactorsList ≠ [] ↔ 1 < n

theorem Nat.eq_of_perm_primeFactorsList {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : a.primeFactorsList.Perm b.primeFactorsList) : a = b

theorem Nat.mem_primeFactorsList_iff_dvd {n p : ℕ} (hn : n ≠ 0) (hp : Prime p) : p ∈ n.primeFactorsList ↔ p ∣ n

theorem Nat.dvd_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ n.primeFactorsList) : p ∣ n

theorem Nat.mem_primeFactorsList {n p : ℕ} (hn : n ≠ 0) : p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n

@[simp]

theorem Nat.mem_primeFactorsList' {n p : ℕ} : p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

theorem Nat.le_of_mem_primeFactorsList {n p : ℕ} (h : p ∈ n.primeFactorsList) : p ≤ n

theorem Nat.primeFactorsList_unique {n : ℕ} {l : List ℕ} (h₁ : l.prod = n) (h₂ : ∀ p ∈ l, Prime p) : l.Perm n.primeFactorsList

Fundamental theorem of arithmetic

theorem Nat.Prime.primeFactorsList_pow {p : ℕ} (hp : Prime p) (n : ℕ) : (p ^ n).primeFactorsList = List.replicate n p

theorem Nat.eq_prime_pow_of_unique_prime_dvd {n p : ℕ} (hpos : n ≠ 0) (h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p) : n = p ^ n.primeFactorsList.length

theorem Nat.perm_primeFactorsList_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a * b).primeFactorsList.Perm (a.primeFactorsList ++ b.primeFactorsList)

For positive a and b, the prime factors of a * b are the union of those of a and b

theorem Nat.perm_primeFactorsList_mul_of_coprime {a b : ℕ} (hab : a.Coprime b) : (a * b).primeFactorsList.Perm (a.primeFactorsList ++ b.primeFactorsList)

For coprime a and b, the prime factors of a * b are the union of those of a and b

theorem Nat.primeFactorsList_sublist_right {n k : ℕ} (h : k ≠ 0) : n.primeFactorsList.Sublist (n * k).primeFactorsList

theorem Nat.primeFactorsList_sublist_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) : n.primeFactorsList.Sublist k.primeFactorsList

theorem Nat.primeFactorsList_subset_right {n k : ℕ} (h : k ≠ 0) : n.primeFactorsList ⊆ (n * k).primeFactorsList

theorem Nat.primeFactorsList_subset_of_dvd {n k : ℕ} (h : n ∣ k) (h' : k ≠ 0) : n.primeFactorsList ⊆ k.primeFactorsList

theorem Nat.dvd_of_primeFactorsList_subperm {a b : ℕ} (ha : a ≠ 0) (h : a.primeFactorsList.Subperm b.primeFactorsList) : a ∣ b

theorem Nat.replicate_subperm_primeFactorsList_iff {a b n : ℕ} (ha : Prime a) (hb : b ≠ 0) : (List.replicate n a).Subperm b.primeFactorsList ↔ a ^ n ∣ b

theorem Nat.mem_primeFactorsList_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) {p : ℕ} : p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

theorem Nat.coprime_primeFactorsList_disjoint {a b : ℕ} (hab : a.Coprime b) : a.primeFactorsList.Disjoint b.primeFactorsList

The sets of factors of coprime a and b are disjoint

theorem Nat.mem_primeFactorsList_mul_of_coprime {a b : ℕ} (hab : a.Coprime b) (p : ℕ) : p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

theorem Nat.mem_primeFactorsList_mul_left {p a b : ℕ} (hpa : p ∈ a.primeFactorsList) (hb : b ≠ 0) : p ∈ (a * b).primeFactorsList

If p is a prime factor of a then p is also a prime factor of a * b for any b > 0

theorem Nat.mem_primeFactorsList_mul_right {p a b : ℕ} (hpb : p ∈ b.primeFactorsList) (ha : a ≠ 0) : p ∈ (a * b).primeFactorsList

If p is a prime factor of b then p is also a prime factor of a * b for any a > 0

theorem Nat.eq_two_pow_or_exists_odd_prime_and_dvd (n : ℕ) : (∃ (k : ℕ), n = 2 ^ k) ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p

theorem Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt {n : ℕ} (n2 : 2 < n) : 4 ∣ n ∨ ∃ (p : ℕ), Prime p ∧ p ∣ n ∧ Odd p