isMultiplicative_zetaMul — Mathlib

English

The function zetaMul χ is multiplicative for any Dirichlet character χ.

Русский

Функция zetaMul χ мультипликативна для любого символа Дирихле χ.

LaTeX

$$$\forall χ:\mathrm{DirichletCharacter}\;\mathbb{C}\;N,\ χ.zetaMul.IsMultiplicative$$$

Lean4

/-- The arithmetic function `zetaMul χ` is multiplicative. -/
theorem isMultiplicative_zetaMul (χ : DirichletCharacter ℂ N) : χ.zetaMul.IsMultiplicative :=
  isMultiplicative_zeta.natCast.mul <| isMultiplicative_toArithmeticFunction χ

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