smul_apply — Mathlib

English

The scalar action of a function with values in R on a function with values in M is given by a Dirichlet-type sum: (f • g)(n) = sum over divisorsAntidiagonal n of f(x.fst) • g(x.snd).

Русский

Действие скаляра над функциями $f$ и $g$ задаётся суммой по диагонали делителей: (f • g)(n) = ∑ f(x₁) • g(x₂).

LaTeX

$$$ (f \\cdot g) \\;? \\,$$$

Lean4

@[simp]
theorem smul_apply {f : ArithmeticFunction R} {g : ArithmeticFunction M} {n : ℕ} :
    (f • g) n = ∑ x ∈ divisorsAntidiagonal n, f x.fst • g x.snd :=
  rfl

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