isMultiplicative_toArithmeticFunction

English

For a Dirichlet character χ modulo N with values in a commutative monoid-with-zero, the arithmetic function associated to χ is multiplicative: χ(mn) = χ(m)χ(n) whenever gcd(m,n)=1.

Русский

Для характеристической функции Дирихле χ модуля N в коммутативном моноиде с нулём соответствующая арифметическая функция мультипликативна: χ(mn) = χ(m)χ(n) при gcd(m,n)=1.

LaTeX

$$$(\text{toArithmeticFunction}(χ \cdot)).IsMultiplicative$$$

Lean4

/-- The arithmetic function associated to a Dirichlet character is multiplicative. -/
theorem isMultiplicative_toArithmeticFunction {N : ℕ} {R : Type*} [CommMonoidWithZero R] (χ : DirichletCharacter R N) :
    (toArithmeticFunction (χ ·)).IsMultiplicative :=
  by
  refine IsMultiplicative.iff_ne_zero.mpr ⟨?_, fun {m} {n} hm hn _ ↦ ?_⟩
  · simp [toArithmeticFunction]
  · simp [toArithmeticFunction, hm, hn]

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