Theorems · Theorem · number theory

Nat.multiplicative_factorization

∀ {β : Type u_1} [inst : CommMonoid β] (f : ℕ → β),
  (∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) →
    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

Defined in

Mathlib.Data.Nat.Factorization.Induction

Cited by

3 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoid