English
For s ∈ C with s ≠ 0, the map n ↦ n^{−s} is a completely multiplicative function on N to C, extending with 0 ↦ 0 and 1 ↦ 1.
Русский
Для комплексного параметра s ≠ 0 отображение n ↦ n^{−s} является полностью мультипликативной функцией на множестве натуральных чисел в комплексные числа, с допуском 0 ↦ 0 и 1 ↦ 1.
LaTeX
$$$\forall s \in \mathbb{C},\; s \neq 0 \Rightarrow n \mapsto n^{-s} \text{ is a completely multiplicative map } \mathbb{N} \to \mathbb{C} \text{ with } 0 \mapsto 0, 1 \mapsto 1.$$$
Lean4
/-- When `s ≠ 0`, the map `n ↦ n^(-s)` is completely multiplicative and vanishes at zero. -/
noncomputable def riemannZetaSummandHom (hs : s ≠ 0) : ℕ →*₀ ℂ
where
toFun n := (n : ℂ) ^ (-s)
map_zero' := by simp [hs]
map_one' := by simp
map_mul' m
n := by simpa only [Nat.cast_mul, ofReal_natCast] using mul_cpow_ofReal_nonneg m.cast_nonneg n.cast_nonneg _
