English
If f is multiplicative with f(1)=1 and f(0)=1, then f(n) equals the product over p^k in the factorization of n of f(p^k) for all n.
Русский
Если f мультипликативна и выполняются f(1)=1, f(0)=1, то для любого n выполняется f(n)=∏_{p^k|n} f(p^k).
LaTeX
$$$\text{If } f: \mathbb{N} \to \beta \text{ is multiplicative with } f(1)=1, f(0)=1,\text{ then } f(n)=\prod_{p^k\mid n} f(p^k).$$$
Lean4
/-- 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 multiplicative_factorization' {β : Type*} [CommMonoid β] (f : ℕ → β)
(h_mult : ∀ x y : ℕ, Coprime x 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) :=
by
obtain rfl | hn := eq_or_ne n 0
· simpa
· exact multiplicative_factorization _ h_mult hf1 hn
