# Documentation

Mathlib.Data.Nat.Factors

# Prime numbers #

This file deals with the factors of natural numbers.

## Important declarations #

def Nat.factors :

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

Equations
Instances For
@[simp]
theorem Nat.factors_zero :
= []
@[simp]
theorem Nat.factors_one :
= []
theorem Nat.prime_of_mem_factors {n : } {p : } (h : p ) :
theorem Nat.pos_of_mem_factors {n : } {p : } (h : p ) :
0 < p
theorem Nat.prod_factors {n : } :
n 0 = n
theorem Nat.factors_prime {p : } (hp : ) :
= [p]
theorem Nat.factors_chain {n : } {a : } :
(∀ (p : ), p na p)List.Chain (fun (x x_1 : ) => x x_1) a ()
theorem Nat.factors_chain_2 (n : ) :
List.Chain (fun (x x_1 : ) => x x_1) 2 ()
theorem Nat.factors_chain' (n : ) :
List.Chain' (fun (x x_1 : ) => x x_1) ()
theorem Nat.factors_sorted (n : ) :
List.Sorted (fun (x x_1 : ) => x x_1) ()
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 : ) :
= [] n = 0 n = 1
theorem Nat.eq_of_perm_factors {a : } {b : } (ha : a 0) (hb : b 0) (h : ) :
a = b
theorem Nat.mem_factors_iff_dvd {n : } {p : } (hn : n 0) (hp : ) :
p p n
theorem Nat.dvd_of_mem_factors {n : } {p : } (h : p ) :
p n
theorem Nat.mem_factors {n : } {p : } (hn : n 0) :
p p n
@[simp]
theorem Nat.mem_factors' {n : } {p : } :
p p n n 0
theorem Nat.le_of_mem_factors {n : } {p : } (h : p ) :
p n
theorem Nat.factors_unique {n : } {l : } (h₁ : = n) (h₂ : pl, ) :
l ~

Fundamental theorem of arithmetic

theorem Nat.Prime.factors_pow {p : } (hp : ) (n : ) :
Nat.factors (p ^ n) =
theorem Nat.eq_prime_pow_of_unique_prime_dvd {n : } {p : } (hpos : n 0) (h : ∀ {d : }, d nd = p) :
n = p ^
theorem Nat.perm_factors_mul {a : } {b : } (ha : a 0) (hb : b 0) :
Nat.factors (a * 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.factors (a * 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) :
theorem Nat.factors_sublist_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
theorem Nat.factors_subset_right {n : } {k : } (h : k 0) :
theorem Nat.factors_subset_of_dvd {n : } {k : } (h : n k) (h' : k 0) :
theorem Nat.dvd_of_factors_subperm {a : } {b : } (ha : a 0) (h : ) :
a b
theorem Nat.mem_factors_mul {a : } {b : } (ha : a 0) (hb : b 0) {p : } :
p Nat.factors (a * b) p p
theorem Nat.coprime_factors_disjoint {a : } {b : } (hab : ) :

The sets of factors of coprime a and b are disjoint

theorem Nat.mem_factors_mul_of_coprime {a : } {b : } (hab : ) (p : ) :
p Nat.factors (a * b) p
theorem Nat.mem_factors_mul_left {p : } {a : } {b : } (hpa : p ) (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 ) (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 : ), 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 n Odd p