LFunction_eq_LSeries — Mathlib

English

For χ and 1 < Re(s), the L-function equals the L-series of the Dirichlet character: LFunction χ s = LSeries (χ ·) s.

Русский

Для χ и 1 < Re(s) выполняется: LFunction χ s = LSeries (χ ·) s.

LaTeX

$$LFunction χ s = LSeries (χ ·) s$$

Lean4

/-- For `1 < re s` the L-function of a Dirichlet character agrees with the sum of the naive Dirichlet
series.
-/
theorem LFunction_eq_LSeries (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < re s) : LFunction χ s = LSeries (χ ·) s :=
  ZMod.LFunction_eq_LSeries χ hs

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