# Documentation

Mathlib.Data.Nat.Factorization.Basic

# Prime factorizations #

n.factorization is the finitely supported function ℕ →₀ ℕ mapping each prime factor of n to its multiplicity in n. For example, since 2000 = 2^4 * 5^3,

• factorization 2000 2 is 4
• factorization 2000 5 is 3
• factorization 2000 k is 0 for all other k : ℕ.

## TODO #

• As discussed in this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/217875/topic/Multiplicity.20in.20the.20naturals We have lots of disparate ways of talking about the multiplicity of a prime in a natural number, including factors.count, padicValNat, multiplicity, and the material in Data/PNat/Factors. Move some of this material to this file, prove results about the relationships between these definitions, and (where appropriate) choose a uniform canonical way of expressing these ideas.

• Moreover, the results here should be generalised to an arbitrary unique factorization monoid with a normalization function, and then deduplicated. The basics of this have been started in RingTheory/UniqueFactorizationDomain.

• Extend the inductions to any NormalizationMonoid with unique factorization.

n.factorization is the finitely supported function ℕ →₀ ℕ mapping each prime factor of n to its multiplicity in n.

Instances For
theorem Nat.factorization_def (n : ) {p : } (pp : ) :
↑() p =
@[simp]
theorem Nat.factors_count_eq {n : } {p : } :
= ↑() p

We can write both n.factorization p and n.factors.count p to represent the power of p in the factorization of n: we declare the former to be the simp-normal form.

theorem Nat.factorization_eq_factors_multiset (n : ) :
= Multiset.toFinsupp ↑()
theorem Nat.multiplicity_eq_factorization {n : } {p : } (pp : ) (hn : n 0) :
= ↑(↑() p)

### Basic facts about factorization #

@[simp]
theorem Nat.factorization_prod_pow_eq_self {n : } (hn : n 0) :
(Finsupp.prod () fun x x_1 => x ^ x_1) = n
theorem Nat.eq_of_factorization_eq {a : } {b : } (ha : a 0) (hb : b 0) (h : ∀ (p : ), ↑() p = ↑() p) :
a = b

Every nonzero natural number has a unique prime factorization

@[simp]
@[simp]
theorem Nat.support_factorization {n : } :
().support =

The support of n.factorization is exactly n.factors.toFinset

theorem Nat.factor_iff_mem_factorization {n : } {p : } :
p ().support p
theorem Nat.prime_of_mem_factorization {n : } {p : } (hp : p ().support) :
theorem Nat.pos_of_mem_factorization {n : } {p : } (hp : p ().support) :
0 < p
theorem Nat.le_of_mem_factorization {n : } {p : } (h : p ().support) :
p n

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

theorem Nat.factorization_eq_zero_iff (n : ) (p : ) :
↑() p = 0 ¬p n n = 0
@[simp]
theorem Nat.factorization_eq_zero_of_non_prime (n : ) {p : } (hp : ) :
↑() p = 0
theorem Nat.factorization_eq_zero_of_not_dvd {n : } {p : } (h : ¬p n) :
↑() p = 0
theorem Nat.factorization_eq_zero_of_lt {n : } {p : } (h : n < p) :
↑() p = 0
@[simp]
theorem Nat.factorization_zero_right (n : ) :
↑() 0 = 0
@[simp]
theorem Nat.factorization_one_right (n : ) :
↑() 1 = 0
theorem Nat.dvd_of_factorization_pos {n : } {p : } (hn : ↑() p 0) :
p n
theorem Nat.Prime.factorization_pos_of_dvd {n : } {p : } (hp : ) (hn : n 0) (h : p n) :
0 < ↑() p
theorem Nat.factorization_eq_zero_of_remainder {p : } {r : } (i : ) (hr : ¬p r) :
↑(Nat.factorization (p * i + r)) p = 0
theorem Nat.factorization_eq_zero_iff_remainder {p : } {r : } (i : ) (pp : ) (hr0 : r 0) :
¬p r ↑(Nat.factorization (p * i + r)) p = 0
theorem Nat.factorization_eq_zero_iff' (n : ) :
n = 0 n = 1

The only numbers with empty prime factorization are 0 and 1

## Lemmas about factorizations of products and powers #

@[simp]
theorem Nat.factorization_mul {a : } {b : } (ha : a 0) (hb : b 0) :

For nonzero a and b, the power of p in a * b is the sum of the powers in a and b

theorem Nat.factorization_mul_support {a : } {b : } (ha : a 0) (hb : b 0) :
(Nat.factorization (a * b)).support = ().support ().support
theorem Nat.prod_factorization_eq_prod_factors {n : } {β : Type u_1} [] (f : β) :
(Finsupp.prod () fun p x => f p) = Finset.prod () fun p => f p

If a product over n.factorization doesn't use the multiplicities of the prime factors then it's equal to the corresponding product over n.factors.toFinset

theorem Nat.factorization_prod {α : Type u_1} {S : } {g : α} (hS : ∀ (x : α), x Sg x 0) :
= Finset.sum S fun x => Nat.factorization (g x)

For any p : ℕ and any function g : α → ℕ that's non-zero on S : Finset α, the power of p in S.prod g equals the sum over x ∈ S of the powers of p in g x. Generalises factorization_mul, which is the special case where S.card = 2 and g = id.

@[simp]
theorem Nat.factorization_pow (n : ) (k : ) :

For any p, the power of p in n^k is k times the power in n

## Lemmas about factorizations of primes and prime powers #

@[simp]
theorem Nat.Prime.factorization {p : } (hp : ) :
= fun₀ | p => 1

The only prime factor of prime p is p itself, with multiplicity 1

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

The multiplicity of prime p in p is 1

theorem Nat.Prime.factorization_pow {p : } {k : } (hp : ) :
Nat.factorization (p ^ k) = fun₀ | p => k

For prime p the only prime factor of p^k is p with multiplicity k

theorem Nat.eq_pow_of_factorization_eq_single {n : } {p : } {k : } (hn : n 0) (h : = fun₀ | p => k) :
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 : ↑() q 0) :
p = q

The only prime factor of prime p is p itself.

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

theorem Nat.prod_pow_factorization_eq_self {f : } (hf : ∀ (p : ), p f.support) :
Nat.factorization (Finsupp.prod f fun x x_1 => x ^ x_1) = f

Any Finsupp f : ℕ →₀ ℕ whose support is in the primes is equal to the factorization of the product ∏ (a : ℕ) in f.support, a ^ f a.

theorem Nat.eq_factorization_iff {n : } {f : } (hn : n 0) (hf : ∀ (p : ), p f.support) :
(Finsupp.prod f fun x x_1 => x ^ x_1) = n
def Nat.factorizationEquiv :
ℕ+ {f | ∀ (p : ), p f.support}

The equiv between ℕ+ and ℕ →₀ ℕ with support in the primes.

Instances For
theorem Nat.factorizationEquiv_inv_apply {f : } (hf : ∀ (p : ), p f.support) :
↑( { val := f, property := hf }) = Finsupp.prod f fun x x_1 => x ^ x_1

### Generalisation of the "even part" and "odd part" of a natural number #

We introduce the notations ord_proj[p] n for the largest power of the prime p that divides n and ord_compl[p] n for the complementary part. The ord naming comes from the $p$-adic order/valuation of a number, and proj and compl are for the projection and complementary projection. The term n.factorization p is the $p$-adic order itself. For example, ord_proj n is the even part of n and ord_compl n is the odd part.

Instances For
Instances For
@[simp]
theorem Nat.ord_proj_of_not_prime (n : ) (p : ) (hp : ) :
p ^ ↑() p = 1
@[simp]
theorem Nat.ord_compl_of_not_prime (n : ) (p : ) (hp : ) :
n / p ^ ↑() p = n
theorem Nat.ord_proj_dvd (n : ) (p : ) :
p ^ ↑() p n
theorem Nat.ord_compl_dvd (n : ) (p : ) :
n / p ^ ↑() p n
theorem Nat.ord_proj_pos (n : ) (p : ) :
0 < p ^ ↑() p
theorem Nat.ord_proj_le {n : } (p : ) (hn : n 0) :
p ^ ↑() p n
theorem Nat.ord_compl_pos {n : } (p : ) (hn : n 0) :
0 < n / p ^ ↑() p
theorem Nat.ord_compl_le (n : ) (p : ) :
n / p ^ ↑() p n
theorem Nat.ord_proj_mul_ord_compl_eq_self (n : ) (p : ) :
p ^ ↑() p * (n / p ^ ↑() p) = n
theorem Nat.ord_proj_mul {a : } {b : } (p : ) (ha : a 0) (hb : b 0) :
p ^ ↑(Nat.factorization (a * b)) p = p ^ ↑() p * p ^ ↑() p
theorem Nat.ord_compl_mul (a : ) (b : ) (p : ) :
a * b / p ^ ↑(Nat.factorization (a * b)) p = a / p ^ ↑() p * (b / p ^ ↑() p)

### Factorization and divisibility #

theorem Nat.dvd_of_mem_factorization {n : } {p : } (h : p ().support) :
p n
theorem Nat.factorization_lt {n : } (p : ) (hn : n 0) :
↑() p < n

A crude upper bound on n.factorization p

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

An upper bound on n.factorization p

theorem Nat.factorization_le_iff_dvd {d : } {n : } (hd : d 0) (hn : n 0) :
d n
theorem Nat.factorization_prime_le_iff_dvd {d : } {n : } (hd : d 0) (hn : n 0) :
(∀ (p : ), ↑() p ↑() p) d n
theorem Nat.pow_succ_factorization_not_dvd {n : } {p : } (hn : n 0) (hp : ) :
¬p ^ (↑() p + 1) n
theorem Nat.Prime.pow_dvd_iff_le_factorization {p : } {k : } {n : } (pp : ) (hn : n 0) :
p ^ k n k ↑() p
theorem Nat.Prime.pow_dvd_iff_dvd_ord_proj {p : } {k : } {n : } (pp : ) (hn : n 0) :
p ^ k n p ^ k p ^ ↑() p
theorem Nat.Prime.dvd_iff_one_le_factorization {p : } {n : } (pp : ) (hn : n 0) :
p n 1 ↑() p
theorem Nat.exists_factorization_lt_of_lt {a : } {b : } (ha : a 0) (hab : a < b) :
p, ↑() p < ↑() p
@[simp]
theorem Nat.factorization_div {d : } {n : } (h : d n) :
theorem Nat.dvd_ord_proj_of_dvd {n : } {p : } (hn : n 0) (pp : ) (h : p n) :
p p ^ ↑() p
theorem Nat.not_dvd_ord_compl {n : } {p : } (hp : ) (hn : n 0) :
¬p n / p ^ ↑() p
theorem Nat.coprime_ord_compl {n : } {p : } (hp : ) (hn : n 0) :
Nat.Coprime p (n / p ^ ↑() p)
theorem Nat.factorization_ord_compl (n : ) (p : ) :
Nat.factorization (n / p ^ ↑() p) =
theorem Nat.dvd_ord_compl_of_dvd_not_dvd {p : } {d : } {n : } (hdn : d n) (hpd : ¬p d) :
d n / p ^ ↑() 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.dvd_iff_div_factorization_eq_tsub {d : } {n : } (hd : d 0) (hdn : d n) :
d n
theorem Nat.ord_proj_dvd_ord_proj_of_dvd {a : } {b : } (hb0 : b 0) (hab : a b) (p : ) :
p ^ ↑() p p ^ ↑() p
theorem Nat.ord_proj_dvd_ord_proj_iff_dvd {a : } {b : } (ha0 : a 0) (hb0 : b 0) :
(∀ (p : ), p ^ ↑() p p ^ ↑() p) a b
theorem Nat.ord_compl_dvd_ord_compl_of_dvd {a : } {b : } (hab : a b) (p : ) :
a / p ^ ↑() p b / p ^ ↑() p
theorem Nat.ord_compl_dvd_ord_compl_iff_dvd (a : ) (b : ) :
(∀ (p : ), a / p ^ ↑() p b / p ^ ↑() 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_prime_factors_dvd (n : ) :
(Finset.prod () fun p => p) n
theorem Nat.factorization_gcd {a : } {b : } (ha_pos : a 0) (hb_pos : b 0) :
theorem Nat.factorization_lcm {a : } {b : } (ha : a 0) (hb : b 0) :
theorem Nat.setOf_pow_dvd_eq_Icc_factorization {n : } {p : } (pp : ) (hn : n 0) :
{i | i 0 p ^ i n} = Set.Icc 1 (↑() p)
theorem Nat.Icc_factorization_eq_pow_dvd (n : ) {p : } (pp : ) :
Finset.Icc 1 (↑() 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 : ) :
↑() p = Finset.card (Finset.filter (fun i => p ^ i n) ())
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_mul_apply_of_coprime {p : } {a : } {b : } (hab : ) :
↑(Nat.factorization (a * b)) p = ↑() p + ↑() p

For coprime a and b, the power of p in a * b is the sum of the powers in a and b

theorem Nat.factorization_mul_of_coprime {a : } {b : } (hab : ) :

For coprime a and b, the power of p in a * b is the sum of the powers in a and b

theorem Nat.factorization_eq_of_coprime_left {p : } {a : } {b : } (hab : ) (hpa : p ) :
↑(Nat.factorization (a * b)) p = ↑() 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 : ) (hpb : p ) :
↑(Nat.factorization (a * b)) p = ↑() 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.factorization_disjoint_of_coprime {a : } {b : } (hab : ) :
Disjoint ().support ().support

The prime factorizations of coprime a and b are disjoint

theorem Nat.factorization_mul_support_of_coprime {a : } {b : } (hab : ) :
(Nat.factorization (a * b)).support = ().support ().support

For coprime a and b the prime factorization a * b is the union of those of a and b

### Induction principles involving factorizations #

def Nat.recOnPrimePow {P : Sort u_1} (h0 : P 0) (h1 : P 1) (h : (a p n : ) → ¬p a0 < nP aP (p ^ n * a)) (a : ) :
P a

Given P 0, P 1 and a way to extend P a to P (p ^ n * a) for prime p not dividing a, we can define P for all natural numbers.

Instances For
def Nat.recOnPosPrimePosCoprime {P : Sort u_1} (hp : (p n : ) → 0 < nP (p ^ n)) (h0 : P 0) (h1 : P 1) (h : (a b : ) → 1 < a1 < bP aP bP (a * b)) (a : ) :
P a

Given P 0, P 1, and P (p ^ n) for positive prime powers, and a way to extend P a and P b to P (a * b) when a, b are positive coprime, we can define P for all natural numbers.

Instances For
def Nat.recOnPrimeCoprime {P : Sort u_1} (h0 : P 0) (hp : (p n : ) → P (p ^ n)) (h : (a b : ) → 1 < a1 < bP aP bP (a * b)) (a : ) :
P a

Given P 0, P (p ^ n) for all prime powers, and a way to extend P a and P b to P (a * b) when a, b are positive coprime, we can define P for all natural numbers.

Instances For
def Nat.recOnMul {P : Sort u_1} (h0 : P 0) (h1 : P 1) (hp : (p : ) → P p) (h : (a b : ) → P aP bP (a * b)) (a : ) :
P a

Given P 0, P 1, P p for all primes, and a way to extend P a and P b to P (a * b), we can define P for all natural numbers.

Instances For
theorem Nat.multiplicative_factorization {β : Type u_1} [] (f : β) (h_mult : ∀ (x y : ), f (x * y) = f x * f y) (hf : f 1 = 1) {n : } :
n 0f n = Finsupp.prod () fun p k => f (p ^ k)

For any multiplicative function f with f 1 = 1 and any n ≠ 0, we can evaluate f n by evaluating f at p ^ k over the factorization of n

theorem Nat.multiplicative_factorization' {β : Type u_1} [] (f : β) (h_mult : ∀ (x y : ), f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) {n : } :
f n = Finsupp.prod () fun p k => f (p ^ k)

For any multiplicative function f with f 1 = 1 and f 0 = 1, we can evaluate f n by evaluating f at p ^ k over the factorization of n

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) :
(Finset.prod () fun p => p ^ ) = n

### Lemmas about factorizations of particular functions #

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

Exactly n / p naturals in [1, n] are multiples of p.

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

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