instMul — Mathlib

English

The product (multiplication) of two arithmetic functions is defined by Dirichlet convolution: (f * g)(n) = sum_{x y = n} f(x) g(y).

Русский

Произведение двух арифметических функций задаётся через свёртку Дирихле: (f * g)(n) = ∑_{xy=n} f(x) g(y).

LaTeX

$$$ (f * g)(n) = \\sum_{x,y:\\, xy=n} f(x) \\; g(y) $$$

Lean4

/-- The Dirichlet convolution of two arithmetic functions `f` and `g` is another arithmetic function
  such that `(f * g) n` is the sum of `f x * g y` over all `(x,y)` such that `x * y = n`. -/
instance [Semiring R] : Mul (ArithmeticFunction R) :=
  ⟨(· • ·)⟩

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