sum_divisorsAntidiagonal_eq_sum_divisors

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

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