Commit 2026-04-02 08:19 6f07e308

View on Github →

feat(NumberTheory): zeros of Riemann zeta on compact sets are finite (#37328) Greetings! This PR proves that any compact subset of ℂ meets the zero set of the Riemann zeta function in only finitely many points (riemannZeta_zeroes_on_Compact_finite). This result in used in https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/issues/750

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

added theorem riemannZeta_eventually_ne_zero_nhds_one

Modified Mathlib/NumberTheory/LSeries/RiemannZeta.lean

added theorem analyticOn_riemannZeta

added theorem differentiableOn_riemannZeta

Created Mathlib/NumberTheory/LSeries/ZetaZeros.lean

added theorem IsCompact.inter_riemannZetaZeros_finite

added theorem isClosed_riemannZetaZeros

added theorem isDiscrete_riemannZetaZeros

added theorem mem_riemannZetaZeros

added def riemannZetaZeros

added theorem tendsto_riemannZeta_cofinite_cocompact