English
The Riemann zeta function does not vanish in the closed half-plane Re s ≥ 1; in particular ζ(1) is nonzero (despite being a pole of related constructions, it is nonzero as a value).
Русский
Функция дзета Римана не имеет нулей в замкнутой полуплоскости Re s ≥ 1; в частности ζ(1) не равна нулю (несмотря на полю), как значение она не нулевая.
LaTeX
$$$\zeta(s) \neq 0 \quad \text{for } \Re(s) \ge 1$$$
Lean4
/-- The Riemann Zeta Function does not vanish on the closed half-plane `re s ≥ 1`.
(Note that the value at `s = 1` is a junk value, which happens to be nonzero.) -/
theorem _root_.riemannZeta_ne_zero_of_one_le_re ⦃s : ℂ⦄ (hs : 1 ≤ s.re) : riemannZeta s ≠ 0 :=
by
rcases eq_or_ne s 1 with rfl | hs₀
· exact riemannZeta_one_ne_zero
· exact LFunction_modOne_eq (χ := 1) ▸ LFunction_ne_zero_of_one_le_re _ (.inr hs₀) hs
