2025-12-27 18:03
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
feat(NumberTheory/ModularForms/EisensteinSeries/Summable): add auxiliary E2 lemmas (#32955) …
Added EisensteinSeries.isLittleO_const_left_of_properSpace_of_discreteTopology