Theorem EisensteinSeries.eisensteinSeriesSIF_apply

Modification history

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