coe_zeta_mul_apply

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.coe_zeta_mul_apply

English

The convolution (ζ * f) evaluated at x equals the sum over divisors of x of f(i).

Русский

Свёртка (ζ * f) в точке x равна сумме по делителям x от f(i).

LaTeX

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

Lean4

theorem coe_zeta_mul_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i :=
  coe_zeta_smul_apply

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru