LSeries_eulerProduct_tprod — Mathlib

English

For DirichletCharacter χ modulo N and Re(s) > 1, ∏' p: Primes, (1 − χ(p) p^{−s})^{−1} = L(χ, s).

Русский

Для Dirichlet-символа χ по модулю N и Re(s) > 1, ∏' p: Primes, (1 − χ(p) p^{−s})^{−1} = L(χ, s).

LaTeX

$$$\prod_{p \in \mathrm{Primes}} \bigl(1 - χ(p) p^{-s}\bigr)^{-1} = L(χ, s).$$$

Lean4

/-- The Euler product for Dirichlet L-series, valid for `s.re > 1`.
This version is stated in terms of `tprod`. -/
theorem LSeries_eulerProduct_tprod {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) :
    ∏' p : Primes, (1 - χ p * (p : ℂ) ^ (-s))⁻¹ = L (↗χ) s :=
  (DirichletCharacter.LSeries_eulerProduct_hasProd χ hs).tprod_eq

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