Commit 2026-06-10 16:01 f430c194

View on Github →

feat(ZetaAsymp): derivative of RiemannZeta at 0 (#40316) Adds deriv_riemannZeta_zero: ζ'(0) = -log(2π) / 2.

Estimated changes

Modified Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

modified theorem completedRiemannZeta_one

modified theorem completedRiemannZeta₀_one

added theorem completedRiemannZeta₀_zero

added theorem deriv_riemannZeta_zero

modified theorem riemannZeta_eventually_ne_zero_nhds_one

modified theorem riemannZeta_one

modified theorem riemannZeta_one_ne_zero