Theorem tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow

Modification history

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