Commit 2024-07-09 13:58 7c9231f6

View on Github →

Eisenstein series are modular forms (#12604) We show Eisenstein series are modular forms.

Estimated changes

Modified Mathlib.lean

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

deleted def EisensteinSeries.eisensteinSeries

added def eisensteinSeries

Created Mathlib/NumberTheory/ModularForms/EisensteinSeries/ModularForm.lean

added def ModularForm.eisensteinSeries_MF