Prime factorizations #

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

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, padic_val_nat, 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 ring_theory/unique_factorization_domain.
Extend the inductions to any normalization_monoid with unique factorization.

source

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.factors.to_finset, to_fun := λ (p : ℕ), ite (nat.prime p) (padic_val_nat p n) 0, mem_support_to_fun := _}

source

theorem nat.factorization_def (n : ℕ) {p : ℕ} (pp : nat.prime p) :

⇑(n.factorization) p = padic_val_nat p n

source

@[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.

source

theorem nat.factorization_eq_factors_multiset (n : ℕ) :

n.factorization = ⇑multiset.to_finsupp ↑(n.factors)

source

theorem nat.multiplicity_eq_factorization {n p : ℕ} (pp : nat.prime p) (hn : n ≠ 0) :

multiplicity p n = ↑(⇑(n.factorization) p)

Basic facts about factorization #

source

@[simp]

theorem nat.factorization_prod_pow_eq_self {n : ℕ} (hn : n ≠ 0) :

n.factorization.prod has_pow.pow = n

source

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

a = b

source

theorem nat.factorization_inj :

set.inj_on nat.factorization {x : ℕ | x ≠ 0}

Every nonzero natural number has a unique prime factorization

source

@[simp]

theorem nat.factorization_zero :

0.factorization = 0

source

@[simp]

theorem nat.factorization_one :

1.factorization = 0

source

@[simp]

theorem nat.support_factorization {n : ℕ} :

n.factorization.support = n.factors.to_finset

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

source

theorem nat.factor_iff_mem_factorization {n p : ℕ} :

p ∈ n.factorization.support ↔ p ∈ n.factors

source

theorem nat.prime_of_mem_factorization {n p : ℕ} (hp : p ∈ n.factorization.support) :

nat.prime p

source

theorem nat.pos_of_mem_factorization {n p : ℕ} (hp : p ∈ n.factorization.support) :

0 < p

source

theorem nat.le_of_mem_factorization {n p : ℕ} (h : p ∈ n.factorization.support) :

p ≤ n

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

source

theorem nat.factorization_eq_zero_iff (n p : ℕ) :

⇑(n.factorization) p = 0 ↔ ¬nat.prime p ∨ ¬p ∣ n ∨ n = 0

source

@[simp]

theorem nat.factorization_eq_zero_of_non_prime (n : ℕ) {p : ℕ} (hp : ¬nat.prime p) :

⇑(n.factorization) p = 0

source

theorem nat.factorization_eq_zero_of_not_dvd {n p : ℕ} (h : ¬p ∣ n) :

⇑(n.factorization) p = 0

source

theorem nat.factorization_eq_zero_of_lt {n p : ℕ} (h : n < p) :

⇑(n.factorization) p = 0

source

@[simp]

theorem nat.factorization_zero_right (n : ℕ) :

⇑(n.factorization) 0 = 0

source

@[simp]

theorem nat.factorization_one_right (n : ℕ) :

⇑(n.factorization) 1 = 0

source

theorem nat.dvd_of_factorization_pos {n p : ℕ} (hn : ⇑(n.factorization) p ≠ 0) :

p ∣ n

source

theorem nat.prime.factorization_pos_of_dvd {n p : ℕ} (hp : nat.prime p) (hn : n ≠ 0) (h : p ∣ n) :

0 < ⇑(n.factorization) p

source

theorem nat.factorization_eq_zero_of_remainder {p r : ℕ} (i : ℕ) (hr : ¬p ∣ r) :

⇑((p * i + r).factorization) p = 0

source

theorem nat.factorization_eq_zero_iff_remainder {p r : ℕ} (i : ℕ) (pp : nat.prime p) (hr0 : r ≠ 0) :

¬p ∣ r ↔ ⇑((p * i + r).factorization) p = 0

source

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 #

source

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

source

theorem nat.factorization_mul_support {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :

(a * b).factorization.support = a.factorization.support ∪ b.factorization.support

source

theorem nat.prod_factorization_eq_prod_factors {n : ℕ} {β : Type u_1} [comm_monoid β] (f : ℕ → β) :

n.factorization.prod (λ (p k : ℕ), f p) = n.factors.to_finset.prod (λ (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.to_finset

source

theorem nat.factorization_prod {α : Type u_1} {S : finset α} {g : α → ℕ} (hS : ∀ (x : α), x ∈ S → g x ≠ 0) :

(S.prod g).factorization = S.sum (λ (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.

source

@[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 #

source

@[simp]

theorem nat.prime.factorization {p : ℕ} (hp : nat.prime p) :

p.factorization = finsupp.single p 1

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

source

@[simp]

theorem nat.prime.factorization_self {p : ℕ} (hp : nat.prime p) :

⇑(p.factorization) p = 1

The multiplicity of prime p in p is 1

source

theorem nat.prime.factorization_pow {p k : ℕ} (hp : nat.prime p) :

(p ^ k).factorization = finsupp.single p k

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

source

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

source

theorem nat.prime.eq_of_factorization_pos {p q : ℕ} (hp : nat.prime p) (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. #

source

theorem nat.prod_pow_factorization_eq_self {f : ℕ →₀ ℕ} (hf : ∀ (p : ℕ), p ∈ f.support → nat.prime p) :

(f.prod has_pow.pow).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.

source

theorem nat.eq_factorization_iff {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf : ∀ (p : ℕ), p ∈ f.support → nat.prime p) :

f = n.factorization ↔ f.prod has_pow.pow = n

source

def nat.factorization_equiv :

ℕ+ ≃ ↥{f : ℕ →₀ ℕ | ∀ (p : ℕ), p ∈ f.support → nat.prime p}

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

Equations

nat.factorization_equiv = {to_fun := λ (_x : ℕ+), nat.factorization_equiv._match_1 _x, inv_fun := λ (_x : ↥{f : ℕ →₀ ℕ | ∀ (p : ℕ), p ∈ f.support → nat.prime p}), nat.factorization_equiv._match_2 _x, left_inv := nat.factorization_equiv._proof_1, right_inv := nat.factorization_equiv._proof_2}
nat.factorization_equiv._match_1 ⟨n, hn⟩ = ⟨n.factorization, _⟩
nat.factorization_equiv._match_2 ⟨f, hf⟩ = ⟨f.prod has_pow.pow, _⟩

source

theorem nat.factorization_equiv_apply (n : ℕ+) :

(⇑nat.factorization_equiv n).val = n.val.factorization

source

theorem nat.factorization_equiv_inv_apply {f : ℕ →₀ ℕ} (hf : ∀ (p : ℕ), p ∈ f.support → nat.prime p) :

(⇑(nat.factorization_equiv.symm) ⟨f, hf⟩).val = f.prod has_pow.pow

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.

source

@[simp]

theorem nat.ord_proj_of_not_prime (n p : ℕ) (hp : ¬nat.prime p) :

p ^ ⇑(n.factorization) p = 1

source

@[simp]

theorem nat.ord_compl_of_not_prime (n p : ℕ) (hp : ¬nat.prime p) :

n / p ^ ⇑(n.factorization) p = n

source

theorem nat.ord_proj_dvd (n p : ℕ) :

p ^ ⇑(n.factorization) p ∣ n

source

theorem nat.ord_compl_dvd (n p : ℕ) :

n / p ^ ⇑(n.factorization) p ∣ n

source

theorem nat.ord_proj_pos (n p : ℕ) :

0 < p ^ ⇑(n.factorization) p

source

theorem nat.ord_proj_le {n : ℕ} (p : ℕ) (hn : n ≠ 0) :

p ^ ⇑(n.factorization) p ≤ n

source

theorem nat.ord_compl_pos {n : ℕ} (p : ℕ) (hn : n ≠ 0) :

0 < n / p ^ ⇑(n.factorization) p

source

theorem nat.ord_compl_le (n p : ℕ) :

n / p ^ ⇑(n.factorization) p ≤ n

source

theorem nat.ord_proj_mul_ord_compl_eq_self (n p : ℕ) :

p ^ ⇑(n.factorization) p * (n / p ^ ⇑(n.factorization) p) = n

source

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

source

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 #

source

theorem nat.dvd_of_mem_factorization {n p : ℕ} (h : p ∈ n.factorization.support) :

p ∣ n

source

theorem nat.factorization_lt {n : ℕ} (p : ℕ) (hn : n ≠ 0) :

⇑(n.factorization) p < n

A crude upper bound on n.factorization p

source

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

source

theorem nat.factorization_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :

d.factorization ≤ n.factorization ↔ d ∣ n

source

theorem nat.factorization_prime_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :

(∀ (p : ℕ), nat.prime p → ⇑(d.factorization) p ≤ ⇑(n.factorization) p) ↔ d ∣ n

source

theorem nat.pow_succ_factorization_not_dvd {n p : ℕ} (hn : n ≠ 0) (hp : nat.prime p) :

¬p ^ (⇑(n.factorization) p + 1) ∣ n

source

theorem nat.factorization_le_factorization_mul_left {a b : ℕ} (hb : b ≠ 0) :

a.factorization ≤ (a * b).factorization

source

theorem nat.factorization_le_factorization_mul_right {a b : ℕ} (ha : a ≠ 0) :

b.factorization ≤ (a * b).factorization

source

theorem nat.prime.pow_dvd_iff_le_factorization {p k n : ℕ} (pp : nat.prime p) (hn : n ≠ 0) :

p ^ k ∣ n ↔ k ≤ ⇑(n.factorization) p

source

theorem nat.prime.pow_dvd_iff_dvd_ord_proj {p k n : ℕ} (pp : nat.prime p) (hn : n ≠ 0) :

p ^ k ∣ n ↔ p ^ k ∣ p ^ ⇑(n.factorization) p

source

theorem nat.prime.dvd_iff_one_le_factorization {p n : ℕ} (pp : nat.prime p) (hn : n ≠ 0) :

p ∣ n ↔ 1 ≤ ⇑(n.factorization) p

source

theorem nat.exists_factorization_lt_of_lt {a b : ℕ} (ha : a ≠ 0) (hab : a < b) :

∃ (p : ℕ), ⇑(a.factorization) p < ⇑(b.factorization) p

source

@[simp]

theorem nat.factorization_div {d n : ℕ} (h : d ∣ n) :

(n / d).factorization = n.factorization - d.factorization

source

theorem nat.dvd_ord_proj_of_dvd {n p : ℕ} (hn : n ≠ 0) (pp : nat.prime p) (h : p ∣ n) :

p ∣ p ^ ⇑(n.factorization) p

source

theorem nat.not_dvd_ord_compl {n p : ℕ} (hp : nat.prime p) (hn : n ≠ 0) :

¬p ∣ n / p ^ ⇑(n.factorization) p

source

theorem nat.coprime_ord_compl {n p : ℕ} (hp : nat.prime p) (hn : n ≠ 0) :

p.coprime (n / p ^ ⇑(n.factorization) p)

source

theorem nat.factorization_ord_compl (n p : ℕ) :

(n / p ^ ⇑(n.factorization) p).factorization = finsupp.erase p n.factorization

source

theorem nat.dvd_ord_compl_of_dvd_not_dvd {p d n : ℕ} (hdn : d ∣ n) (hpd : ¬p ∣ d) :

d ∣ n / p ^ ⇑(n.factorization) p

source

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

source

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

source

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

source

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

source

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

source

theorem nat.ord_compl_dvd_ord_compl_iff_dvd (a b : ℕ) :

(∀ (p : ℕ), a / p ^ ⇑(a.factorization) p ∣ b / p ^ ⇑(b.factorization) p) ↔ a ∣ b

source

theorem nat.dvd_iff_prime_pow_dvd_dvd (n d : ℕ) :

d ∣ n ↔ ∀ (p k : ℕ), nat.prime p → p ^ k ∣ d → p ^ k ∣ n

source

theorem nat.prod_prime_factors_dvd (n : ℕ) :

n.factors.to_finset.prod (λ (p : ℕ), p) ∣ n

source

theorem nat.factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) :

(a.gcd b).factorization = a.factorization ⊓ b.factorization

source

theorem nat.factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :

(a.lcm b).factorization = a.factorization ⊔ b.factorization

source

theorem nat.sum_factors_gcd_add_sum_factors_mul {β : Type u_1} [add_comm_monoid β] (m n : ℕ) (f : ℕ → β) :

(m.gcd n).factors.to_finset.sum f + (m * n).factors.to_finset.sum f = m.factors.to_finset.sum f + n.factors.to_finset.sum f

source

theorem nat.prod_factors_gcd_mul_prod_factors_mul {β : Type u_1} [comm_monoid β] (m n : ℕ) (f : ℕ → β) :

(m.gcd n).factors.to_finset.prod f * (m * n).factors.to_finset.prod f = m.factors.to_finset.prod f * n.factors.to_finset.prod f

source

theorem nat.set_of_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : nat.prime p) (hn : n ≠ 0) :

{i : ℕ | i ≠ 0 ∧ p ^ i ∣ n} = set.Icc 1 (⇑(n.factorization) p)

source

theorem nat.Icc_factorization_eq_pow_dvd (n : ℕ) {p : ℕ} (pp : nat.prime p) :

finset.Icc 1 (⇑(n.factorization) p) = finset.filter (λ (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.

source

theorem nat.factorization_eq_card_pow_dvd (n : ℕ) {p : ℕ} (pp : nat.prime p) :

⇑(n.factorization) p = (finset.filter (λ (i : ℕ), p ^ i ∣ n) (finset.Ico 1 n)).card

source

theorem nat.Ico_filter_pow_dvd_eq {n p b : ℕ} (pp : nat.prime p) (hn : n ≠ 0) (hb : n ≤ p ^ b) :

finset.filter (λ (i : ℕ), p ^ i ∣ n) (finset.Ico 1 n) = finset.filter (λ (i : ℕ), p ^ i ∣ n) (finset.Icc 1 b)

Factorization and coprimes #

source

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

source

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

source

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.

source

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.

source

theorem nat.factorization_disjoint_of_coprime {a b : ℕ} (hab : a.coprime b) :

disjoint a.factorization.support b.factorization.support

The prime factorizations of coprime a and b are disjoint

source

theorem nat.factorization_mul_support_of_coprime {a b : ℕ} (hab : a.coprime b) :

(a * b).factorization.support = a.factorization.support ∪ b.factorization.support

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

Induction principles involving factorizations #

source

def nat.rec_on_prime_pow {P : ℕ → Sort u_1} (h0 : P 0) (h1 : P 1) (h : Π (a p n : ℕ), nat.prime p → ¬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

nat.rec_on_prime_pow h0 h1 h = λ (a : ℕ), a.strong_rec_on (λ (n : ℕ), nat.rec_on_prime_pow._match_1 h0 h1 h n)
nat.rec_on_prime_pow._match_1 h0 h1 h (k + 2) = λ (hk : Π (m : ℕ), m < k + 2 → P m), let p : ℕ := (k + 2).min_fac, t : ℕ := list.count p (k + 2).factors in _.mpr (h ((k + 2) / p ^ t) p t _ _ _ (hk ((k + 2) / p ^ t) _))
nat.rec_on_prime_pow._match_1 h0 h1 h 1 = λ (_x : Π (m : ℕ), m < 1 → P m), h1
nat.rec_on_prime_pow._match_1 h0 h1 h 0 = λ (_x : Π (m : ℕ), m < 0 → P m), h0

source

def nat.rec_on_pos_prime_pos_coprime {P : ℕ → Sort u_1} (hp : Π (p n : ℕ), nat.prime p → 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

nat.rec_on_pos_prime_pos_coprime hp h0 h1 h = nat.rec_on_prime_pow h0 h1 (λ (a p n : ℕ) (hp' : nat.prime p) (hpa : ¬p ∣ a) (hn : 0 < n) (hPa : P a), dite (a = 1) (λ (ha1 : a = 1), _.mpr (_.mpr (hp p n hp' hn))) (λ (ha1 : ¬a = 1), h (p ^ n) a _ _ _ (hp p n hp' hn) hPa))

source

def nat.rec_on_prime_coprime {P : ℕ → Sort u_1} (h0 : P 0) (hp : Π (p n : ℕ), nat.prime p → 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.rec_on_prime_coprime h0 hp h = nat.rec_on_pos_prime_pos_coprime (λ (p n : ℕ) (h : nat.prime p) (_x : 0 < n), hp p n h) h0 (hp 2 0 nat.prime_two) h

source

def nat.rec_on_mul {P : ℕ → Sort u_1} (h0 : P 0) (h1 : P 1) (hp : Π (p : ℕ), nat.prime p → 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.rec_on_mul h0 h1 hp h = let hp : Π (p n : ℕ), nat.prime p → P (p ^ n) := λ (p n : ℕ) (hp' : nat.prime p), nat.rec_on_mul._match_1 h1 hp h p hp' n in nat.rec_on_prime_coprime h0 hp (λ (a b : ℕ) (_x : 1 < a) (_x : 1 < b) (_x : a.coprime b), h a b)
nat.rec_on_mul._match_1 h1 hp h p hp' (n + 1) = h p (p ^ n.add 0) (hp p hp') (nat.rec_on_mul._match_1 h1 hp h p hp' n)
nat.rec_on_mul._match_1 h1 hp h p hp' 0 = h1

source

theorem nat.multiplicative_factorization {β : Type u_1} [comm_monoid β] (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 (λ (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

source

theorem nat.multiplicative_factorization' {β : Type u_1} [comm_monoid β] (f : ℕ → β) (h_mult : ∀ (x y : ℕ), x.coprime y → f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) {n : ℕ} :

f n = n.factorization.prod (λ (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

source