Theorem EisensteinSeries.summable_inv_of_isBigO_rpow_inv

Modification history

2025-06-26 13:35
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
feat: Add more Summability results needed for Eisenstein series. (#26005) …
Added EisensteinSeries.summable_inv_of_isBigO_rpow_invView on Github →