Theorem summable_eisSummand

Modification history

2025-11-14 13:33

Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

feat: Eisenstein q exp identity (#27606) …

Added summable_eisSummand View on Github →