Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.completedRiemannZeta_ne_zero_of_one_lt_re

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/ZetaFiniteOrder.lean:454 to 466

Source documentation

In the half-plane of absolute convergence, the completed zeta function does not vanish.

Exact Lean statement

theorem completedRiemannZeta_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) :
    completedRiemannZeta s ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem completedRiemannZeta_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) :    completedRiemannZeta s ≠ 0 := by  have hGamma_ne0 : Gammaℝ s ≠ 0 :=    Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs)  have hzeta_ne0 : riemannZeta s ≠ 0 := riemannZeta_ne_zero_of_one_lt_re hs  have hΛ_def : completedRiemannZeta s = riemannZeta s * Gammaℝ s := by    have hzeta_def := riemannZeta_def_of_ne_zero (s := s) (ne_zero_of_one_lt_re hs)    have hzeta_mul := congrArg (fun x => x * Gammaℝ s) hzeta_def    have : riemannZeta s * Gammaℝ s = completedRiemannZeta s := by      simpa [div_eq_mul_inv, mul_assoc, hGamma_ne0] using hzeta_mul    exact this.symm  rw [hΛ_def]  exact mul_ne_zero hzeta_ne0 hGamma_ne0