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 Mathlib/RingTheory/UniqueFactorizationDomain/.

• Extend the inductions to any NormalizationMonoid with unique factorization.

def Nat.factorization (n : ℕ) : ℕ →₀ ℕ

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

Equations

• n.factorization = { support := n.primeFactors, toFun := fun (p : ℕ) => if Nat.Prime p then padicValNat p n else 0, mem_support_toFun := ⋯ }

@[simp]

theorem Nat.support_factorization (n : ℕ) : n.factorization.support = n.primeFactors

The support of n.factorization is exactly n.primeFactors.

theorem Nat.factorization_def (n : ℕ) {p : ℕ} (pp : Prime p) : n.factorization p = padicValNat p n

@[simp]

theorem Nat.primeFactorsList_count_eq {n p : ℕ} : List.count p n.primeFactorsList = n.factorization 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_primeFactorsList_multiset (n : ℕ) : n.factorization = Multiset.toFinsupp ↑n.primeFactorsList

theorem Nat.Prime.factorization_pos_of_dvd {n p : ℕ} (hp : Prime p) (hn : n ≠ 0) (h : p ∣ n) : 0 < n.factorization p

theorem Nat.multiplicity_eq_factorization {n p : ℕ} (pp : Prime p) (hn : n ≠ 0) : multiplicity p n = n.factorization p

Basic facts about factorization

@[simp]

theorem Nat.prod_factorization_pow_eq_self {n : ℕ} (hn : n ≠ 0) : (n.factorization.prod fun (x1 x2 : ℕ) => x1 ^ x2) = n

@[deprecated Nat.prod_factorization_pow_eq_self (since := "2026-03-19")]

theorem Nat.factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) : (n.factorization.prod fun (x1 x2 : ℕ) => x1 ^ x2) = n

Alias of Nat.prod_factorization_pow_eq_self.

theorem Nat.eq_of_factorization_eq {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : ℕ), a.factorization p = b.factorization p) : a = b

theorem Nat.eq_of_factorization_eq' {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : a.factorization = b.factorization) : a = b

theorem Nat.factorization_inj : Set.InjOn factorization {x : ℕ | x ≠ 0}

Every nonzero natural number has a unique prime factorization

@[simp]

theorem Nat.factorization_zero : factorization 0 = 0

@[simp]

theorem Nat.factorization_one : factorization 1 = 0

Lemmas characterising when n.factorization p = 0

theorem Nat.factorization_eq_zero_iff (n p : ℕ) : n.factorization p = 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

@[simp]

theorem Nat.factorization_eq_zero_of_not_prime (n : ℕ) {p : ℕ} (hp : ¬Prime p) : n.factorization p = 0

@[simp]

theorem Nat.factorization_zero_right (n : ℕ) : n.factorization 0 = 0

@[simp]

theorem Nat.factorization_one_right (n : ℕ) : n.factorization 1 = 0

theorem Nat.factorization_eq_zero_of_not_dvd {n p : ℕ} (h : ¬p ∣ n) : n.factorization p = 0

theorem Nat.factorization_eq_zero_of_remainder {p r : ℕ} (i : ℕ) (hr : ¬p ∣ r) : (p * i + r).factorization p = 0

Lemmas about factorizations of products and powers

@[simp]

theorem Nat.factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (a * b).factorization = a.factorization + b.factorization

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_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : d.factorization ≤ n.factorization ↔ d ∣ n

theorem Nat.factorization_prod {α : Type u_1} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) : (S.prod g).factorization = ∑ x ∈ S, (g x).factorization

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 = 2 and g = id.

@[simp]

theorem Nat.factorization_pow (n k : ℕ) : (n ^ k).factorization = k • n.factorization

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 : Prime p) : p.factorization = Finsupp.single p 1

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

theorem Nat.Prime.factorization_pow {p k : ℕ} (hp : Prime p) : (p ^ k).factorization = Finsupp.single p k

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

theorem Nat.pow_succ_factorization_not_dvd {n p : ℕ} (hn : n ≠ 0) (hp : Prime p) : ¬p ^ (n.factorization p + 1) ∣ n

theorem Nat.factorization_minFac_ne_zero {n : ℕ} (hn : 1 < n) : n.factorization n.minFac ≠ 0

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

theorem Nat.prod_pow_factorization_eq_self {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.support, Prime p) : (f.prod fun (x1 x2 : ℕ) => x1 ^ x2).factorization = f

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

theorem Nat.eq_factorization_iff {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : ∀ p ∈ f.support, Prime p) : f = n.factorization ↔ (f.prod fun (x1 x2 : ℕ) => x1 ^ x2) = n

theorem Nat.factorization_prod_pow_eq_self_of_le_factorization {n : ℕ} {f : ℕ →₀ ℕ} (hf : f ≤ n.factorization) : (f.prod fun (x1 x2 : ℕ) => x1 ^ x2).factorization = f

theorem Nat.prod_pow_dvd_of_le_factorization {n : ℕ} {f : ℕ →₀ ℕ} (hf : f ≤ n.factorization) : (f.prod fun (x1 x2 : ℕ) => x1 ^ x2) ∣ n

theorem Nat.dvd_prod_pow_of_factorization_le {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : n.factorization ≤ f) : n ∣ f.prod fun (x1 x2 : ℕ) => x1 ^ x2

theorem Nat.dvd_iff_exists_le_factorization {n d : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun (x1 x2 : ℕ) => x1 ^ x2

def Nat.factorizationEquiv : ℕ+ ≃ { f : ℕ →₀ ℕ // ∀ p ∈ f.support, Prime p }

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Nat.factorizationEquiv_apply (x✝ : ℕ+) : factorizationEquiv x✝ = match x✝ with | ⟨n, property⟩ => ⟨n.factorization, ⋯⟩

@[simp]

theorem Nat.factorizationEquiv_symm_apply_coe (x✝ : { f : ℕ →₀ ℕ // ∀ p ∈ f.support, Prime p }) : ↑(factorizationEquiv.symm x✝) = (↑x✝).prod fun (x1 x2 : ℕ) => x1 ^ x2

Factorization and coprimes

theorem Nat.factorization_mul_apply_of_coprime {p a b : ℕ} (hab : a.Coprime b) : (a * b).factorization p = a.factorization p + b.factorization 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 : a.Coprime b) : (a * b).factorization = a.factorization + b.factorization

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

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

def Nat.«termOrdProj[_]_» : Lean.ParserDescr

We introduce the notations ordProj[p] n for the largest power of the prime p that divides n and ordCompl[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, ordProj[2] n is the even part of n and ordCompl[2] n is the odd part.

Equations

• One or more equations did not get rendered due to their size.

def Nat.«termOrdCompl[_]_» : Lean.ParserDescr

We introduce the notations ordProj[p] n for the largest power of the prime p that divides n and ordCompl[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, ordProj[2] n is the even part of n and ordCompl[2] n is the odd part.

Equations

• One or more equations did not get rendered due to their size.

theorem Nat.ordProj_dvd (n p : ℕ) : p ^ n.factorization p ∣ n

theorem Nat.ordProj_dvd_ordProj_iff_dvd {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a ∣ b

Factorization LCM definitions

def Nat.factorizationLCMLeft (a b : ℕ) : ℕ

If a = ∏ pᵢ ^ nᵢ and b = ∏ pᵢ ^ mᵢ, then factorizationLCMLeft = ∏ pᵢ ^ kᵢ, where kᵢ = nᵢ if mᵢ ≤ nᵢ and 0 otherwise. Note that the product is over the divisors of lcm a b, so if one of a or b is 0 then the result is 1.

Equations

• a.factorizationLCMLeft b = (a.lcm b).factorization.prod fun (p n : ℕ) => if b.factorization p ≤ a.factorization p then p ^ n else 1

def Nat.factorizationLCMRight (a b : ℕ) : ℕ

If a = ∏ pᵢ ^ nᵢ and b = ∏ pᵢ ^ mᵢ, then factorizationLCMRight = ∏ pᵢ ^ kᵢ, where kᵢ = mᵢ if nᵢ < mᵢ and 0 otherwise. Note that the product is over the divisors of lcm a b, so if one of a or b is 0 then the result is 1.

Note that factorizationLCMRight a b is not factorizationLCMLeft b a: the difference is that in factorizationLCMLeft a b there are the primes whose exponent in a is bigger or equal than the exponent in b, while in factorizationLCMRight a b there are the primes whose exponent in b is strictly bigger than in a. For example factorizationLCMLeft 2 2 = 2, but factorizationLCMRight 2 2 = 1.

Equations

• a.factorizationLCMRight b = (a.lcm b).factorization.prod fun (p n : ℕ) => if b.factorization p ≤ a.factorization p then 1 else p ^ n