LFunction_modOne_eq — Mathlib

English

If χ is the Dirichlet character modulo 1, then its L-function equals the Riemann zeta function: LFunction χ = ζ.

Русский

Если χ — единственный характер модуль 1, то его L-функция равна дзета-функции: LFunction χ = ζ.

LaTeX

$$LFunction χ = ζ ∀ χ : DirichletCharacter ℂ 1$$

Lean4

/-- The L-function of the (unique) Dirichlet character mod 1 is the Riemann zeta function.
(Compare `DirichletCharacter.LSeries_modOne_eq`.)
-/
@[simp]
theorem LFunction_modOne_eq {χ : DirichletCharacter ℂ 1} : LFunction χ = riemannZeta := by ext;
  rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]

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