Theorems · Theorem · number theory

ArithmeticFunction.IsMultiplicative.multiplicative_factorization

∀ {R : Type u_1} [inst : CommMonoidWithZero R] (f : ArithmeticFunction R),
  f.IsMultiplicative → ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k)

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

Defined in

Mathlib.NumberTheory.ArithmeticFunction.Defs

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZero