riemannZeta_eulerProduct_tprod — Mathlib

English

For Re(s) > 1, the Euler product in tprod form: ∏' p: Primes, (1 - p^{−s})^{−1} = ζ(s).

Русский

Для Re(s) > 1 в форме tprod: ∏' p: Primes, (1 - p^{−s})^{−1} = ζ(s).

LaTeX

$$$\forall s\ (\Re(s)>1)\; \prod_{p \in \mathrm{Primes}} (1 - p^{-s})^{-1} = \zeta(s).$$$

Lean4

/-- The Euler product for the Riemann ζ function, valid for `s.re > 1`.
This version is stated in terms of `tprod`. -/
theorem riemannZeta_eulerProduct_tprod (hs : 1 < s.re) : ∏' p : Primes, (1 - (p : ℂ) ^ (-s))⁻¹ = riemannZeta s :=
  (riemannZeta_eulerProduct_hasProd hs).tprod_eq

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