Theorem EisensteinSeries.eisensteinSeriesSIF_mdifferentiable

Modification history

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