LSeries_zeta_ne_zero_of_one_lt_re

English

For Re(s) > 1, the L-series L((↗ζ), s) is nonzero: L((↗ζ), s) ≠ 0.

Русский

Для Re(s) > 1 L-ряд дзеты не равен нулю: L((↗ζ), s) ≠ 0.

LaTeX

$$$1 < \\operatorname{Re}(s) \\Rightarrow L(↗ζ,s) \\neq 0$$$

Lean4

/-- The L-series of the arithmetic function `ζ` does not vanish on the right half-plane
`re s > 1`. -/
theorem LSeries_zeta_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : L (↗ζ) s ≠ 0 := fun h ↦ by
  simpa [h, -zeta_apply] using LSeries_zeta_mul_Lseries_moebius hs

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