Theorem riemannZeta_one_ne_zero

Modification history

2026-06-10 16:01
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
feat(ZetaAsymp): derivative of RiemannZeta at 0 (#40316) …
Modified riemannZeta_one_ne_zeroView on Github →
2024-06-04 08:01
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
feat(NumberTheory/Harmonic): explicit formula for `ζ 1` (#13434) …
Added riemannZeta_one_ne_zeroView on Github →