Theorem riemannZeta_eventually_ne_zero_nhds_one

Modification history

2026-06-10 16:01
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
feat(ZetaAsymp): derivative of RiemannZeta at 0 (#40316) …
Modified riemannZeta_eventually_ne_zero_nhds_oneView on Github →
2026-04-02 08:19
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
feat(NumberTheory): zeros of Riemann zeta on compact sets are finite (#37328) …
Added riemannZeta_eventually_ne_zero_nhds_oneView on Github →