Theorem ZetaAsymptotics.termSum_one

Modification history

2026-05-28 09:36

Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

chore(NumberTheory/Harmonic/ZetaAsymp): remove underscores in definitions (#39948) …

Added ZetaAsymptotics.termSum_one View on Github →