riemannZeta_ne_zero_of_one_lt_re — Mathlib

English

If Re(s) > 1, then the Riemann zeta function ζ(s) ≠ 0.

Русский

Если Re(s) > 1, то дзета-функция ζ(s) не равна нулю.

LaTeX

$$$1 < \\operatorname{Re}(s) \\Rightarrow \\operatorname{riemannZeta}(s) \\neq 0$$$

Lean4

/-- The Riemann Zeta Function does not vanish on the half-plane `re s > 1`. -/
theorem riemannZeta_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : riemannZeta s ≠ 0 :=
  LSeries_one_eq_riemannZeta hs ▸ LSeries_one_ne_zero_of_one_lt_re hs

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