English
For a Dirichlet character χ modulo N and s ≠ 0, the function n ↦ χ(n) n^{−s} is a completely multiplicative map ℕ → ℂ vanishing at 0.
Русский
ДляDirichlet-символа χ по модулю N и s ≠ 0 функция n ↦ χ(n) n^{−s} является полной мультипликативной отображением ℕ → ℂ, где 0 отображается в 0.
LaTeX
$$$\forall n,m \in \mathbb{N},\; χ(mn)(mn)^{-s} = χ(m)χ(n) m^{-s} n^{-s},\; (0)^{-s}=0,\; χ(0)=0,$ что свидетельствует, что $n \mapsto χ(n) n^{-s}$ — полная мультипликативность с нулём на нуле.$$
Lean4
/-- When `χ` is a Dirichlet character and `s ≠ 0`, the map `n ↦ χ n * n^(-s)` is completely
multiplicative and vanishes at zero. -/
noncomputable def dirichletSummandHom {n : ℕ} (χ : DirichletCharacter ℂ n) (hs : s ≠ 0) : ℕ →*₀ ℂ
where
toFun n := χ n * (n : ℂ) ^ (-s)
map_zero' := by simp [hs]
map_one' := by simp
map_mul' m
n := by
simp_rw [← ofReal_natCast]
simpa only [Nat.cast_mul, IsUnit.mul_iff, not_and, map_mul, ofReal_mul,
mul_cpow_ofReal_nonneg m.cast_nonneg n.cast_nonneg _] using mul_mul_mul_comm ..
