English
Let f be an arithmetic function valued in a semiring; the left-hand sum over the divisor-antidiagonal of x, with the zero-left factor ignored, equals the divisor-sum ∑_{d|x} f(d).
Русский
Пусть f — арифметическая функция, принимающая значения в полугруппе; сумма по антидиагонали делителей x с нулевым слева фактором равна сумме по делителям x: ∑_{d|x} f(d).
LaTeX
$$$$ \sum_{(a,b) \in x.{\rm divisorsAntidiagonal}} \mathbf{1}_{a \neq 0} f(b) = \sum_{d \mid x} f(d) $$$$
Lean4
/-- `@[simp]`-normal form of `coe_zeta_smul_apply`. -/
@[simp]
theorem sum_divisorsAntidiagonal_eq_sum_divisors {M} [Semiring R] [AddCommMonoid M] [MulAction R M]
{f : ArithmeticFunction M} {x : ℕ} :
(∑ x ∈ x.divisorsAntidiagonal, if x.1 = 0 then (0 : R) • f x.2 else f x.2) = ∑ i ∈ divisors x, f i :=
by
rw [← coe_zeta_smul_apply (R := R)]
simp