Source indexedtheorem · leanprover/lean4:v4.32.0

completedRiemannZeta₀_nontrivial

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaValues.lean:101 to 112

Source documentation

The entire completed zeta function Λ₀ is not identically zero.

Exact Lean statement

theorem completedRiemannZeta₀_nontrivial : ∃ z : ℂ, completedRiemannZeta₀ z ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem completedRiemannZeta₀_nontrivial : ∃ z : ℂ, completedRiemannZeta₀ z ≠ 0 := by  refine ⟨(2 : ℂ), ?_⟩  have hpi_ne3 : (Real.pi : ℂ) ≠ (3 : ℂ) := by    intro h'    have hpi' : (Real.pi : ℝ) = (3 : ℝ) := by      simpa using congrArg Complex.re h'    have hirr : Irrational Real.pi := by simp    exact (hirr.ne_nat 3) (by simp at hpi')  have hnum : ((Real.pi : ℂ) - 3) ≠ 0 := sub_ne_zero.2 hpi_ne3  have hden : (6 : ℂ) ≠ 0 := by norm_num  have : ((Real.pi : ℂ) - 3) / 6 ≠ 0 := div_ne_zero hnum hden  simpa [completedRiemannZeta₀_two] using this