English
Let f be an arithmetic function with values in a module M over a semiring R. The x-th value of the zeta-function acting on f equals the sum of f over all divisors of x: (ζ • f)(x) = ∑_{i|x} f(i).
Русский
Пусть f — арифметическая функция, принимающая значения в модуле M над полугруппой R. Значение функции при x после применения ζ к f равно сумме f по делителям x: (ζ • f)(x) = ∑_{d|x} f(d).
LaTeX
$$$$ ((\zeta : \ArithmeticFunction R) \cdot f)(x) = \sum_{i \mid x} f(i) $$$$
Lean4
theorem coe_zeta_smul_apply {M} [Semiring R] [AddCommMonoid M] [MulAction R M] {f : ArithmeticFunction M} {x : ℕ} :
((↑ζ : ArithmeticFunction R) • f) x = ∑ i ∈ divisors x, f i :=
by
rw [smul_apply]
trans ∑ i ∈ divisorsAntidiagonal x, f i.snd
· refine sum_congr rfl fun i hi => ?_
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]
· rw [← map_div_left_divisors, sum_map, Function.Embedding.coeFn_mk]
