English
If f is a multiplicative function with f(1)=1, then for any nonzero n, f(n) equals the product over primes p of f(p^{v_p(n)}), where v_p(n) denotes the p-adic valuation (exponent of p in n).
Русский
Пусть f — мультипликативная функция с f(1)=1. Тогда для любого ненулевого n выполняется равенство
f(n) = ∏_{p} f(p^{v_p(n)}).
LaTeX
$$$\text{If } f:\mathbb{N}\to\beta\text{ is multiplicative with } f(1)=1,\text{ then for } n\neq 0,\ f(n)=\prod_{p} f(p^{v_p(n)}).$$$
Lean4
theorem prime_composite_induction {motive : ℕ → Prop} (zero : motive 0) (one : motive 1)
(prime : ∀ p : ℕ, p.Prime → motive p) (composite : ∀ a, 2 ≤ a → motive a → ∀ b, 2 ≤ b → motive b → motive (a * b))
(n : ℕ) : motive n := by
refine induction_on_primes zero one ?_ _
rintro p (_ | _ | a) hp ha
· simpa
· simpa using prime _ hp
· exact composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha
