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.

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 p.Prime 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 : p.Prime) : n.factorization p = padicValNat p n

@[simp]

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

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

Basic facts about factorization

@[simp]

theorem Nat.factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) : (n.factorization.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 : ℕ), a.factorization p = b.factorization p) : a = b

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

Every nonzero natural number has a unique prime factorization

@[simp]

theorem Nat.factorization_zero : Nat.factorization 0 = 0

@[simp]

theorem Nat.factorization_one : Nat.factorization 1 = 0

Lemmas characterising when n.factorization p = 0

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

@[simp]

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

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

theorem Nat.factorization_eq_zero_of_lt {n : ℕ} {p : ℕ} (h : n < 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.dvd_of_factorization_pos {n : ℕ} {p : ℕ} (hn : n.factorization p ≠ 0) : p ∣ n

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

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

theorem Nat.factorization_eq_zero_iff_remainder {p : ℕ} {r : ℕ} (i : ℕ) (pp : p.Prime) (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

@[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.prod_factorization_eq_prod_primeFactors {n : ℕ} {β : Type u_1} [CommMonoid β] (f : ℕ → ℕ → β) : n.factorization.prod f = n.primeFactors.prod fun (p : ℕ) => 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} [CommMonoid β] (f : ℕ → β) : (n.primeFactors.prod fun (p : ℕ) => f p) = n.factorization.prod fun (p x : ℕ) => f p

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

theorem Nat.factorization_prod {α : Type u_1} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) : (S.prod g).factorization = S.sum fun (x : α) => (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.card = 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 : p.Prime) : p.factorization = Finsupp.single p 1

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

@[simp]

theorem Nat.Prime.factorization_self {p : ℕ} (hp : p.Prime) : p.factorization p = 1

The multiplicity of prime p in p is 1

theorem Nat.Prime.factorization_pow {p : ℕ} {k : ℕ} (hp : p.Prime) : (p ^ k).factorization = Finsupp.single 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 : n.factorization = Finsupp.single 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 : p.Prime) (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.prod_pow_factorization_eq_self {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.support, p.Prime) : (f.prod fun (x x_1 : ℕ) => x ^ x_1).factorization = 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 ∈ f.support, p.Prime) : f = n.factorization ↔ (f.prod fun (x x_1 : ℕ) => x ^ x_1) = n

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

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

Equations

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

theorem Nat.factorizationEquiv_apply (n : ℕ+) : ↑(Nat.factorizationEquiv n) = (↑n).factorization

theorem Nat.factorizationEquiv_inv_apply {f : ℕ →₀ ℕ} (hf : ∀ p ∈ f.support, p.Prime) : ↑(Nat.factorizationEquiv.symm ⟨f, hf⟩) = f.prod 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[2] n is the even part of n and ord_compl[2] n is the odd part.

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

Equations

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

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

Equations

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

@[simp]

theorem Nat.ord_proj_of_not_prime (n : ℕ) (p : ℕ) (hp : ¬p.Prime) : p ^ n.factorization p = 1

@[simp]

theorem Nat.ord_compl_of_not_prime (n : ℕ) (p : ℕ) (hp : ¬p.Prime) : n / p ^ n.factorization p = n

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

theorem Nat.factorization_prime_le_iff_dvd {d : ℕ} {n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : (∀ (p : ℕ), p.Prime → d.factorization p ≤ n.factorization p) ↔ d ∣ n

theorem Nat.pow_succ_factorization_not_dvd {n : ℕ} {p : ℕ} (hn : n ≠ 0) (hp : p.Prime) : ¬p ^ (n.factorization p + 1) ∣ 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 : p.Prime) (hn : n ≠ 0) : p ^ k ∣ n ↔ k ≤ n.factorization p

theorem Nat.Prime.pow_dvd_iff_dvd_ord_proj {p : ℕ} {k : ℕ} {n : ℕ} (pp : p.Prime) (hn : n ≠ 0) : p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p

theorem Nat.Prime.dvd_iff_one_le_factorization {p : ℕ} {n : ℕ} (pp : p.Prime) (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 : p.Prime) (h : p ∣ n) : p ∣ p ^ n.factorization p

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

theorem Nat.coprime_ord_compl {n : ℕ} {p : ℕ} (hp : p.Prime) (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.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.Prime → p ^ k ∣ d → p ^ k ∣ n

theorem Nat.prod_primeFactors_dvd (n : ℕ) : (n.primeFactors.prod fun (p : ℕ) => 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

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

@[simp]

theorem Nat.factorizationLCMLeft_zero_left (b : ℕ) : Nat.factorizationLCMLeft 0 b = 1

@[simp]

theorem Nat.factorizationLCMLeft_zero_right (a : ℕ) : a.factorizationLCMLeft 0 = 1

@[simp]

theorem Nat.factorizationLCRight_zero_left (b : ℕ) : Nat.factorizationLCMRight 0 b = 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} [AddCommMonoid β] (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} [CommMonoid β] (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 : p.Prime) (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 : p.Prime) : Finset.Icc 1 (n.factorization p) = Finset.filter (fun (i : ℕ) => p ^ i ∣ n) (Finset.Ico 1 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.Prime) : n.factorization p = (Finset.filter (fun (i : ℕ) => p ^ i ∣ n) (Finset.Ico 1 n)).card

theorem Nat.Ico_filter_pow_dvd_eq {n : ℕ} {p : ℕ} {b : ℕ} (pp : p.Prime) (hn : n ≠ 0) (hb : n ≤ p ^ b) : Finset.filter (fun (i : ℕ) => p ^ i ∣ n) (Finset.Ico 1 n) = Finset.filter (fun (i : ℕ) => p ^ i ∣ n) (Finset.Icc 1 b)

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

theorem Nat.factorization_eq_of_coprime_left {p : ℕ} {a : ℕ} {b : ℕ} (hab : a.Coprime b) (hpa : p ∈ a.factors) : (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.factors) : (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.

Induction principles involving factorizations

def Nat.recOnPrimePow {P : ℕ → Sort u_1} (h0 : P 0) (h1 : P 1) (h : (a p n : ℕ) → p.Prime → ¬p ∣ a → 0 < n → P a → P (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.

Equations

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

def Nat.recOnPosPrimePosCoprime {P : ℕ → Sort u_1} (hp : (p n : ℕ) → p.Prime → 0 < n → P (p ^ n)) (h0 : P 0) (h1 : P 1) (h : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → P a → P b → P (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.

Equations

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

def Nat.recOnPrimeCoprime {P : ℕ → Sort u_1} (h0 : P 0) (hp : (p n : ℕ) → p.Prime → P (p ^ n)) (h : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → P a → P b → P (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.

Equations

• Nat.recOnPrimeCoprime h0 hp h a = Nat.recOnPosPrimePosCoprime (fun (p n : ℕ) (h : p.Prime) (x : 0 < n) => hp p n h) h0 (hp 2 0 Nat.prime_two) h a

def Nat.recOnMul {P : ℕ → Sort u_1} (h0 : P 0) (h1 : P 1) (hp : (p : ℕ) → p.Prime → P p) (h : (a b : ℕ) → P a → P b → P (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.

Equations

• Nat.recOnMul h0 h1 hp h a = Nat.recOnPrimeCoprime h0 (Nat.recOnMul.hp'' h1 hp h) (fun (a b : ℕ) (x : 1 < a) (x : 1 < b) (x : a.Coprime b) => h a b) a

def Nat.recOnMul.hp'' {P : ℕ → Sort u_1} (h1 : P 1) (hp : (p : ℕ) → p.Prime → P p) (h : (a b : ℕ) → P a → P b → P (a * b)) (p : ℕ) (n : ℕ) (hp' : p.Prime) : P (p ^ n)

The predicate holds on prime powers

Equations

• Nat.recOnMul.hp'' h1 hp h p 0 hp' = h1
• Nat.recOnMul.hp'' h1 hp h p n_2.succ hp' = h (p.pow n_2) p (Nat.recOnMul.hp'' h1 hp h p n_2 hp') (hp p hp')

theorem Nat.multiplicative_factorization {β : Type u_1} [CommMonoid β] (f : ℕ → β) (h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) (hf : f 1 = 1) {n : ℕ} : n ≠ 0 → f n = n.factorization.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' {n : ℕ} {β : Type u_1} [CommMonoid β] (f : ℕ → β) (h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) : f n = n.factorization.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 : ℕ), p.Prime → padicValNat p a = padicValNat p b

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.filter Nat.Prime (Finset.range m)).prod fun (p : ℕ) => p ^ padicValNat p n) = n

Lemmas about factorizations of particular functions

theorem Nat.card_multiples (n : ℕ) (p : ℕ) : (Finset.filter (fun (e : ℕ) => p ∣ e + 1) (Finset.range n)).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) (Finset.Ioc 0 n)).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.