zetaMul — Mathlib

English

For a Dirichlet character χ, zetaMul χ is defined as the Dirichlet convolution of the constant function 1 with χ, viewed as an arithmetic function.

Русский

Для символа Дирихле χ zetaMul задается как свертка константной функции 1 с χ, как арифметическая функция.

LaTeX

$$$\mathrm{zetaMul}(χ) = \zeta * toArithmeticFunction (χ \cdot)$$$

Lean4

/-- The complex-valued arithmetic function that is the convolution of the constant
function `1` with `χ`. -/
def zetaMul (χ : DirichletCharacter ℂ N) : ArithmeticFunction ℂ :=
  .zeta * toArithmeticFunction (χ ·)

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