Theorem summable_prod_eisSummand

Modification history

2025-11-14 13:33
Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean
feat: Eisenstein q exp identity (#27606) …
Added summable_prod_eisSummandView on Github →