Theorem ZetaAsymptotics.term_sum_one

Modification history

2026-05-28 09:36
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
chore(NumberTheory/Harmonic/ZetaAsymp): remove underscores in definitions (#39948) …
Deleted ZetaAsymptotics.term_sum_oneView on Github →
2024-04-18 08:21
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
feat(NumberTheory/Harmonic): asymptotics of Riemann zeta as s → 1 (#11794) …
Added ZetaAsymptotics.term_sum_oneView on Github →