Theorem tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries

Modification history

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