mul_apply — Mathlib

English

For any f,g in ArithmeticFunction R, (f * g)(n) = sum over divisorsAntidiagonal n of f x.fst * g x.snd.

Русский

Для любых f,g в ArithmeticFunction R, (f * g)(n) = ∑_{x ∈ divisorsAntidiagonal(n)} f x.fst · g x.snd.

LaTeX

$$$ (f * g)(n) = \\sum_{x ∈ divisorsAntidiagonal(n)} f\\,x.fst \\cdot g\\,x.snd$$$

Lean4

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

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