multiplicative_factorization — Mathlib

English

A multiplicative function is determined by its values on prime powers: f(n) = ∏_{p^k∣n} f(p^k).

Русский

Мультипликативная функция определяется значениями на простых степенях: f(n) = ∏_{p^k∣n} f(p^k).

LaTeX

$$$f(n) = \prod_{p^k \mid n} f(p^k) \qquad(n\neq 0)$$$

Lean4

/-- 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` -/
theorem multiplicative_factorization [CommMonoidWithZero R] (f : ArithmeticFunction R) (hf : f.IsMultiplicative) {n : ℕ}
    (hn : n ≠ 0) : f n = n.factorization.prod fun p k => f (p ^ k) :=
  Nat.multiplicative_factorization f (fun _ _ => hf.2) hf.1 hn

Похожие утверждения