Theorem EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF

Modification history

2026-02-11 09:57
Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean
chore: fix some names around Eisenstein series (#35055) …
Added EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIFView on Github →