Theorem completedRiemannZeta₀_one

Modification history

2026-06-10 16:01

Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

feat(ZetaAsymp): derivative of RiemannZeta at 0 (#40316) …

Modified completedRiemannZeta₀_one View on Github →

2024-06-04 08:01

Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

feat(NumberTheory/Harmonic): explicit formula for `ζ 1` (#13434) …

Added completedRiemannZeta₀_one View on Github →