Commit 2026-02-11 09:57 dbff9859

View on Github →

chore: fix some names around Eisenstein series (#35055) Per the naming convention,

eisensteinSeries_MF should be eisensteinSeriesMF,
eisensteinSeries_SIF should be eisensteinSeriesSIF, and
eisensteinSeries_SIF_MDifferentiable should use suffix _mdifferentiable.

Estimated changes

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean

added def ModularForm.eisensteinSeriesMF

deleted def ModularForm.eisensteinSeries_MF

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

added def EisensteinSeries.eisensteinSeriesSIF

added theorem EisensteinSeries.eisensteinSeriesSIF_apply

deleted def EisensteinSeries.eisensteinSeries_SIF

deleted theorem EisensteinSeries.eisensteinSeries_SIF_apply

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

added theorem EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF

deleted theorem EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean

added theorem EisensteinSeries.eisensteinSeriesSIF_mdifferentiable

deleted theorem EisensteinSeries.eisensteinSeries_SIF_MDifferentiable

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean