data.nat.factors

# Prime numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[simp]
theorem nat.factors_zero  :
@[simp]
theorem nat.factors_one  :
theorem nat.pos_of_mem_factors {n p : } (h : p n.factors) :
0 < p
theorem nat.prod_factors {n : } :
n 0 n.factors.prod = n
theorem nat.factors_prime {p : } (hp : nat.prime p) :
p.factors = [p]
theorem nat.factors_chain {n a : } :
( (p : ), p n a p)
theorem nat.factors_chain_2 (n : ) :
theorem nat.factors_chain' (n : ) :
theorem nat.factors_sorted (n : ) :
theorem nat.factors_add_two (n : ) :
(n + 2).factors = (n + 2).min_fac :: ((n + 2) / (n + 2).min_fac).factors

factors can be constructed inductively by extracting min_fac, 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.factors ~ b.factors) :
a = b
theorem nat.mem_factors_iff_dvd {n p : } (hn : n 0) (hp : nat.prime p) :
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) :
theorem nat.le_of_mem_factors {n p : } (h : p n.factors) :
p n
theorem nat.factors_unique {n : } {l : list } (h₁ : l.prod = n) (h₂ : (p : ), p l ) :

Fundamental theorem of arithmetic

theorem nat.prime.factors_pow {p : } (hp : nat.prime p) (n : ) :
(p ^ n).factors =
theorem nat.eq_prime_pow_of_unique_prime_dvd {n p : } (hpos : n 0) (h : {d : }, d n d = p) :
theorem nat.perm_factors_mul {a b : } (ha : a 0) (hb : b 0) :

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

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.factors <+~ b.factors) :
a b
theorem nat.mem_factors_mul {a b : } (ha : a 0) (hb : b 0) {p : } :
theorem nat.coprime_factors_disjoint {a b : } (hab : a.coprime b) :

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 : ) :
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 n odd p