zeta_mul_apply — Mathlib

English

Let f be an arithmetic function with values in the natural numbers. Then for every x ∈ ℕ, (ζ * f)(x) = ∑_{i ∣ x} f(i).

Русский

Пусть f — арифметическая функция, принимающая значения в натуральных числах. Тогда для каждого x ∈ ℕ выполнено (ζ * f)(x) = ∑_{i ∣ x} f(i).

LaTeX

$$$$ (\zeta * f)(x) = \sum_{i \mid x} f(i) $$$$

Lean4

theorem zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i := by
  rw [← natCoe_nat ζ, coe_zeta_mul_apply]

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