# 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 :

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

Equations
• = []
• = []
• k.succ.succ.factors = (k + 2).minFac :: ((k + 2) / (k + 2).minFac).factors
Instances For
@[simp]
theorem Nat.factors_zero :
= []
@[simp]
theorem Nat.factors_one :
= []
@[simp]
theorem Nat.factors_two :
= [2]
theorem Nat.prime_of_mem_factors {n : } {p : } (h : p n.factors) :
p.Prime
theorem Nat.pos_of_mem_factors {n : } {p : } (h : p n.factors) :
0 < p
theorem Nat.prod_factors {n : } :
n 0n.factors.prod = n
theorem Nat.factors_prime {p : } (hp : p.Prime) :
p.factors = [p]
theorem Nat.factors_chain {n : } {a : } :
(∀ (p : ), p.Primep na p)List.Chain (fun (x x_1 : ) => x x_1) a n.factors
theorem Nat.factors_chain_2 (n : ) :
List.Chain (fun (x x_1 : ) => x x_1) 2 n.factors
theorem Nat.factors_chain' (n : ) :
List.Chain' (fun (x x_1 : ) => x x_1) n.factors
theorem Nat.factors_sorted (n : ) :
List.Sorted (fun (x x_1 : ) => x x_1) n.factors
theorem Nat.factors_add_two (n : ) :
(n + 2).factors = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).factors

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

@[simp]
theorem Nat.factors_eq_nil (n : ) :
n.factors = [] n = 0 n = 1
theorem Nat.eq_of_perm_factors {a : } {b : } (ha : a 0) (hb : b 0) (h : a.factors.Perm b.factors) :
a = b
theorem Nat.mem_factors_iff_dvd {n : } {p : } (hn : n 0) (hp : p.Prime) :
p n.factors p n
theorem Nat.dvd_of_mem_factors {n : } {p : } (h : p n.factors) :
p n
theorem Nat.mem_factors {n : } {p : } (hn : n 0) :
p n.factors p.Prime p n
@[simp]
theorem Nat.mem_factors' {n : } {p : } :
p n.factors p.Prime p n n 0
theorem Nat.le_of_mem_factors {n : } {p : } (h : p n.factors) :
p n
theorem Nat.factors_unique {n : } {l : } (h₁ : l.prod = n) (h₂ : pl, p.Prime) :
l.Perm n.factors

Fundamental theorem of arithmetic

theorem Nat.Prime.factors_pow {p : } (hp : p.Prime) (n : ) :
(p ^ n).factors =
theorem Nat.eq_prime_pow_of_unique_prime_dvd {n : } {p : } (hpos : n 0) (h : ∀ {d : }, d.Primed nd = p) :
n = p ^ n.factors.length
theorem Nat.perm_factors_mul {a : } {b : } (ha : a 0) (hb : b 0) :
(a * b).factors.Perm (a.factors ++ b.factors)

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 : a.Coprime b) :
(a * b).factors.Perm (a.factors ++ b.factors)

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) :
n.factors.Sublist (n * k).factors
theorem Nat.factors_sublist_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
n.factors.Sublist k.factors
theorem Nat.factors_subset_right {n : } {k : } (h : k 0) :
n.factors (n * k).factors
theorem Nat.factors_subset_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
n.factors k.factors
theorem Nat.dvd_of_factors_subperm {a : } {b : } (ha : a 0) (h : a.factors.Subperm b.factors) :
a b
theorem Nat.replicate_subperm_factors_iff {a : } {b : } {n : } (ha : a.Prime) (hb : b 0) :
().Subperm b.factors a ^ n b
theorem Nat.mem_factors_mul {a : } {b : } (ha : a 0) (hb : b 0) {p : } :
p (a * b).factors p a.factors p b.factors
theorem Nat.coprime_factors_disjoint {a : } {b : } (hab : a.Coprime b) :
a.factors.Disjoint b.factors

The sets of factors of coprime a and b are disjoint

theorem Nat.mem_factors_mul_of_coprime {a : } {b : } (hab : a.Coprime b) (p : ) :
p (a * b).factors p a.factors b.factors
theorem Nat.mem_factors_mul_left {p : } {a : } {b : } (hpa : p a.factors) (hb : b 0) :
p (a * b).factors

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 b.factors) (ha : a 0) :
p (a * b).factors

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 : ), p.Prime p n Odd p
theorem Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt {n : } (n2 : 2 < n) :
4 n ∃ (p : ), p.Prime p n Odd p