# Basic lemmas on prime factorizations #

## Lemmas characterising when n.factorization p = 0#

theorem Nat.factorization_eq_zero_of_lt {n : } {p : } (h : n < p) :
n.factorization p = 0
@[simp]
theorem Nat.factorization_one_right (n : ) :
n.factorization 1 = 0
theorem Nat.dvd_of_factorization_pos {n : } {p : } (hn : n.factorization p 0) :
p n
theorem Nat.factorization_eq_zero_iff_remainder {p : } {r : } (i : ) (pp : ) (hr0 : r 0) :
¬p r (p * i + r).factorization p = 0
theorem Nat.factorization_eq_zero_iff' (n : ) :
n.factorization = 0 n = 0 n = 1

The only numbers with empty prime factorization are 0 and 1

## Lemmas about factorizations of products and powers #

theorem Nat.prod_factorization_eq_prod_primeFactors {n : } {β : Type u_1} [] (f : β) :
n.factorization.prod f = pn.primeFactors, f p (n.factorization p)

A product over n.factorization can be written as a product over n.primeFactors;

theorem Nat.prod_primeFactors_prod_factorization {n : } {β : Type u_1} [] (f : β) :
pn.primeFactors, f p = n.factorization.prod fun (p x : ) => f p

A product over n.primeFactors can be written as a product over n.factorization;

## Lemmas about factorizations of primes and prime powers #

@[simp]
theorem Nat.Prime.factorization_self {p : } (hp : ) :
p.factorization p = 1

The multiplicity of prime p in p is 1

theorem Nat.eq_pow_of_factorization_eq_single {n : } {p : } {k : } (hn : n 0) (h : n.factorization = ) :
n = p ^ k

If the factorization of n contains just one number p then n is a power of p

theorem Nat.Prime.eq_of_factorization_pos {p : } {q : } (hp : ) (h : p.factorization q 0) :
p = q

The only prime factor of prime p is p itself.

### Equivalence between ℕ+ and ℕ →₀ ℕ with support in the primes. #

theorem Nat.eq_factorization_iff {n : } {f : } (hn : n 0) (hf : pf.support, ) :
f = n.factorization (f.prod fun (x x_1 : ) => x ^ x_1) = n
theorem Nat.factorizationEquiv_inv_apply {f : } (hf : pf.support, ) :
( f, hf) = f.prod fun (x x_1 : ) => x ^ x_1
@[simp]
theorem Nat.ord_proj_of_not_prime (n : ) (p : ) (hp : ) :
p ^ n.factorization p = 1
@[simp]
theorem Nat.ord_compl_of_not_prime (n : ) (p : ) (hp : ) :
n / p ^ n.factorization p = n
theorem Nat.ord_compl_dvd (n : ) (p : ) :
n / p ^ n.factorization p n
theorem Nat.ord_proj_pos (n : ) (p : ) :
0 < p ^ n.factorization p
theorem Nat.ord_proj_le {n : } (p : ) (hn : n 0) :
p ^ n.factorization p n
theorem Nat.ord_compl_pos {n : } (p : ) (hn : n 0) :
0 < n / p ^ n.factorization p
theorem Nat.ord_compl_le (n : ) (p : ) :
n / p ^ n.factorization p n
theorem Nat.ord_proj_mul_ord_compl_eq_self (n : ) (p : ) :
p ^ n.factorization p * (n / p ^ n.factorization p) = n
theorem Nat.ord_proj_mul {a : } {b : } (p : ) (ha : a 0) (hb : b 0) :
p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p
theorem Nat.ord_compl_mul (a : ) (b : ) (p : ) :
a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

### Factorization and divisibility #

theorem Nat.factorization_lt {n : } (p : ) (hn : n 0) :
n.factorization p < n

A crude upper bound on n.factorization p

theorem Nat.factorization_le_of_le_pow {n : } {p : } {b : } (hb : n p ^ b) :
n.factorization p b

An upper bound on n.factorization p

theorem Nat.factorization_prime_le_iff_dvd {d : } {n : } (hd : d 0) (hn : n 0) :
(∀ (p : ), d.factorization p n.factorization p) d n
theorem Nat.factorization_le_factorization_mul_left {a : } {b : } (hb : b 0) :
a.factorization (a * b).factorization
theorem Nat.factorization_le_factorization_mul_right {a : } {b : } (ha : a 0) :
b.factorization (a * b).factorization
theorem Nat.Prime.pow_dvd_iff_le_factorization {p : } {k : } {n : } (pp : ) (hn : n 0) :
p ^ k n k n.factorization p
theorem Nat.Prime.pow_dvd_iff_dvd_ord_proj {p : } {k : } {n : } (pp : ) (hn : n 0) :
p ^ k n p ^ k p ^ n.factorization p
theorem Nat.Prime.dvd_iff_one_le_factorization {p : } {n : } (pp : ) (hn : n 0) :
p n 1 n.factorization p
theorem Nat.exists_factorization_lt_of_lt {a : } {b : } (ha : a 0) (hab : a < b) :
∃ (p : ), a.factorization p < b.factorization p
@[simp]
theorem Nat.factorization_div {d : } {n : } (h : d n) :
(n / d).factorization = n.factorization - d.factorization
theorem Nat.dvd_ord_proj_of_dvd {n : } {p : } (hn : n 0) (pp : ) (h : p n) :
p p ^ n.factorization p
theorem Nat.not_dvd_ord_compl {n : } {p : } (hp : ) (hn : n 0) :
¬p n / p ^ n.factorization p
theorem Nat.coprime_ord_compl {n : } {p : } (hp : ) (hn : n 0) :
p.Coprime (n / p ^ n.factorization p)
theorem Nat.factorization_ord_compl (n : ) (p : ) :
(n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization
theorem Nat.dvd_ord_compl_of_dvd_not_dvd {p : } {d : } {n : } (hdn : d n) (hpd : ¬p d) :
d n / p ^ n.factorization p
theorem Nat.exists_eq_pow_mul_and_not_dvd {n : } (hn : n 0) (p : ) (hp : p 1) :
∃ (e : ) (n' : ), ¬p n' n = p ^ e * n'

If n is a nonzero natural number and p ≠ 1, then there are natural numbers e and n' such that n' is not divisible by p and n = p^e * n'.

theorem Nat.exists_eq_two_pow_mul_odd {n : } (hn : n 0) :
∃ (k : ) (m : ), Odd m n = 2 ^ k * m

Any nonzero natural number is the product of an odd part m and a power of two 2 ^ k.

theorem Nat.dvd_iff_div_factorization_eq_tsub {d : } {n : } (hd : d 0) (hdn : d n) :
d n (n / d).factorization = n.factorization - d.factorization
theorem Nat.ord_proj_dvd_ord_proj_of_dvd {a : } {b : } (hb0 : b 0) (hab : a b) (p : ) :
p ^ a.factorization p p ^ b.factorization p
theorem Nat.ord_proj_dvd_ord_proj_iff_dvd {a : } {b : } (ha0 : a 0) (hb0 : b 0) :
(∀ (p : ), p ^ a.factorization p p ^ b.factorization p) a b
theorem Nat.ord_compl_dvd_ord_compl_of_dvd {a : } {b : } (hab : a b) (p : ) :
a / p ^ a.factorization p b / p ^ b.factorization p
theorem Nat.ord_compl_dvd_ord_compl_iff_dvd (a : ) (b : ) :
(∀ (p : ), a / p ^ a.factorization p b / p ^ b.factorization p) a b
theorem Nat.dvd_iff_prime_pow_dvd_dvd (n : ) (d : ) :
d n ∀ (p k : ), p ^ k dp ^ k n
theorem Nat.prod_primeFactors_dvd (n : ) :
pn.primeFactors, p n
theorem Nat.factorization_gcd {a : } {b : } (ha_pos : a 0) (hb_pos : b 0) :
(a.gcd b).factorization = a.factorization b.factorization
theorem Nat.factorization_lcm {a : } {b : } (ha : a 0) (hb : b 0) :
(a.lcm b).factorization = a.factorization b.factorization
@[simp]
theorem Nat.factorizationLCMLeft_zero_right (a : ) :
a.factorizationLCMLeft 0 = 1
@[simp]
theorem Nat.factorizationLCMRight_zero_right (a : ) :
a.factorizationLCMRight 0 = 1
theorem Nat.factorizationLCMLeft_pos (a : ) (b : ) :
0 < a.factorizationLCMLeft b
theorem Nat.factorizationLCMRight_pos (a : ) (b : ) :
0 < a.factorizationLCMRight b
theorem Nat.coprime_factorizationLCMLeft_factorizationLCMRight (a : ) (b : ) :
(a.factorizationLCMLeft b).Coprime (a.factorizationLCMRight b)
theorem Nat.factorizationLCMLeft_mul_factorizationLCMRight {a : } {b : } (ha : a 0) (hb : b 0) :
a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b
theorem Nat.factorizationLCMLeft_dvd_left (a : ) (b : ) :
a.factorizationLCMLeft b a
theorem Nat.factorizationLCMRight_dvd_right (a : ) (b : ) :
a.factorizationLCMRight b b
theorem Nat.sum_primeFactors_gcd_add_sum_primeFactors_mul {β : Type u_1} [] (m : ) (n : ) (f : β) :
(m.gcd n).primeFactors.sum f + (m * n).primeFactors.sum f = m.primeFactors.sum f + n.primeFactors.sum f
theorem Nat.prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type u_1} [] (m : ) (n : ) (f : β) :
(m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f
theorem Nat.setOf_pow_dvd_eq_Icc_factorization {n : } {p : } (pp : ) (hn : n 0) :
{i : | i 0 p ^ i n} = Set.Icc 1 (n.factorization p)
theorem Nat.Icc_factorization_eq_pow_dvd (n : ) {p : } (pp : ) :
Finset.Icc 1 (n.factorization p) = Finset.filter (fun (i : ) => p ^ i n) ()

The set of positive powers of prime p that divide n is exactly the set of positive natural numbers up to n.factorization p.

theorem Nat.factorization_eq_card_pow_dvd (n : ) {p : } (pp : ) :
n.factorization p = (Finset.filter (fun (i : ) => p ^ i n) ()).card
theorem Nat.Ico_filter_pow_dvd_eq {n : } {p : } {b : } (pp : ) (hn : n 0) (hb : n p ^ b) :
Finset.filter (fun (i : ) => p ^ i n) () = Finset.filter (fun (i : ) => p ^ i n) ()

### Factorization and coprimes #

theorem Nat.factorization_eq_of_coprime_left {p : } {a : } {b : } (hab : a.Coprime b) (hpa : p a.primeFactorsList) :
(a * b).factorization p = a.factorization p

If p is a prime factor of a then the power of p in a is the same that in a * b, for any b coprime to a.

theorem Nat.factorization_eq_of_coprime_right {p : } {a : } {b : } (hab : a.Coprime b) (hpb : p b.primeFactorsList) :
(a * b).factorization p = b.factorization p

If p is a prime factor of b then the power of p in b is the same that in a * b, for any a coprime to b.

theorem Nat.eq_iff_prime_padicValNat_eq (a : ) (b : ) (ha : a 0) (hb : b 0) :
a = b ∀ (p : ), =

Two positive naturals are equal if their prime padic valuations are equal

theorem Nat.prod_pow_prime_padicValNat (n : ) (hn : n 0) (m : ) (pr : n < m) :
p, p ^ = n

### Lemmas about factorizations of particular functions #

theorem Nat.card_multiples (n : ) (p : ) :
(Finset.filter (fun (e : ) => p e + 1) ()).card = n / p

Exactly n / p naturals in [1, n] are multiples of p. See Nat.card_multiples' for an alternative spelling of the statement.

theorem Nat.Ioc_filter_dvd_card_eq_div (n : ) (p : ) :
(Finset.filter (fun (x : ) => p x) ()).card = n / p

Exactly n / p naturals in (0, n] are multiples of p.

theorem Nat.card_multiples' (N : ) (n : ) :
(Finset.filter (fun (k : ) => k 0 n k) (Finset.range N.succ)).card = N / n

There are exactly ⌊N/n⌋ positive multiples of n that are ≤ N. See Nat.card_multiples for a "shifted-by-one" version.