Prime numbers

This file deals with the factors of natural numbers.

Important declarations

• Nat.factors n: the prime factorization of n
• Nat.factors_unique: uniqueness of the prime factorisation

def Nat.factors : ℕ → List ℕ

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

Equations

• Nat.factors 0 = []
• Nat.factors 1 = []
• Nat.factors (Nat.succ (Nat.succ k)) = let m := Nat.minFac (k + 2); let_fun this := ⋯; m :: Nat.factors ((k + 2) / m)

@[simp]

theorem Nat.factors_zero : Nat.factors 0 = []

@[simp]

theorem Nat.factors_one : Nat.factors 1 = []

theorem Nat.prime_of_mem_factors {n : ℕ} {p : ℕ} (h : p ∈ Nat.factors n) : Nat.Prime p

theorem Nat.pos_of_mem_factors {n : ℕ} {p : ℕ} (h : p ∈ Nat.factors n) : 0 < p

theorem Nat.prod_factors {n : ℕ} : n ≠ 0 → List.prod (Nat.factors n) = n

theorem Nat.factors_prime {p : ℕ} (hp : Nat.Prime p) : Nat.factors p = [p]

theorem Nat.factors_chain {n : ℕ} {a : ℕ} : (∀ (p : ℕ), Nat.Prime p → p ∣ n → a ≤ p) → List.Chain (fun (x x_1 : ℕ) => x ≤ x_1) a (Nat.factors n)

theorem Nat.factors_chain_2 (n : ℕ) : List.Chain (fun (x x_1 : ℕ) => x ≤ x_1) 2 (Nat.factors n)

theorem Nat.factors_chain' (n : ℕ) : List.Chain' (fun (x x_1 : ℕ) => x ≤ x_1) (Nat.factors n)

theorem Nat.factors_sorted (n : ℕ) : List.Sorted (fun (x x_1 : ℕ) => x ≤ x_1) (Nat.factors n)

theorem Nat.factors_add_two (n : ℕ) : Nat.factors (n + 2) = Nat.minFac (n + 2) :: Nat.factors ((n + 2) / Nat.minFac (n + 2))

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

@[simp]

theorem Nat.factors_eq_nil (n : ℕ) : Nat.factors n = [] ↔ n = 0 ∨ n = 1

theorem Nat.eq_of_perm_factors {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : List.Perm (Nat.factors a) (Nat.factors b)) : a = b

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

theorem Nat.dvd_of_mem_factors {n : ℕ} {p : ℕ} (h : p ∈ Nat.factors n) : p ∣ n

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

@[simp]

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

theorem Nat.le_of_mem_factors {n : ℕ} {p : ℕ} (h : p ∈ Nat.factors n) : p ≤ n

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

Fundamental theorem of arithmetic

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

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

theorem Nat.perm_factors_mul {a : ℕ} {b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : List.Perm (Nat.factors (a * b)) (Nat.factors a ++ Nat.factors b)

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

theorem Nat.perm_factors_mul_of_coprime {a : ℕ} {b : ℕ} (hab : Nat.Coprime a b) : List.Perm (Nat.factors (a * b)) (Nat.factors a ++ Nat.factors b)

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

theorem Nat.factors_sublist_right {n : ℕ} {k : ℕ} (h : k ≠ 0) : List.Sublist (Nat.factors n) (Nat.factors (n * k))

theorem Nat.factors_sublist_of_dvd {n : ℕ} {k : ℕ} (h : n ∣ k) (h' : k ≠ 0) : List.Sublist (Nat.factors n) (Nat.factors k)

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

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

theorem Nat.dvd_of_factors_subperm {a : ℕ} {b : ℕ} (ha : a ≠ 0) (h : List.Subperm (Nat.factors a) (Nat.factors b)) : a ∣ b

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

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

theorem Nat.coprime_factors_disjoint {a : ℕ} {b : ℕ} (hab : Nat.Coprime a b) : List.Disjoint (Nat.factors a) (Nat.factors b)

The sets of factors of coprime a and b are disjoint

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

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

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_factors_mul_right {p : ℕ} {a : ℕ} {b : ℕ} (hpb : p ∈ Nat.factors b) (ha : a ≠ 0) : p ∈ Nat.factors (a * b)

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 : ℕ), Nat.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 : ℕ), Nat.Prime p ∧ p ∣ n ∧ Odd p