Commit 2024-07-09 17:23 6b9e877b

View on Github →

Chore: Rename files with Eisenstein series stuff. (#14572) Accidentally created a Mathlib/NumberTheory/ModularForms/EisensteinSeries/ModularForm.lean file name. Made it a Basic.lean file and made the previous into a Defs.lean

Estimated changes

Modified Mathlib.lean

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

deleted def EisensteinSeries.eisSummand

deleted theorem EisensteinSeries.eisSummand_SL2_apply

deleted def EisensteinSeries.eisensteinSeries_SIF

deleted theorem EisensteinSeries.eisensteinSeries_SIF_apply

deleted theorem EisensteinSeries.eisensteinSeries_slash_apply

deleted def EisensteinSeries.gammaSet

deleted def EisensteinSeries.gammaSetEquiv

deleted theorem EisensteinSeries.gammaSet_one_eq

deleted def EisensteinSeries.gammaSet_one_equiv

deleted theorem EisensteinSeries.pairwise_disjoint_gammaSet

deleted theorem EisensteinSeries.vecMul_SL2_mem_gammaSet

added def ModularForm.eisensteinSeries_MF

deleted def eisensteinSeries

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

added def EisensteinSeries.eisSummand

added theorem EisensteinSeries.eisSummand_SL2_apply

added def EisensteinSeries.eisensteinSeries_SIF

added theorem EisensteinSeries.eisensteinSeries_SIF_apply

added theorem EisensteinSeries.eisensteinSeries_slash_apply

added def EisensteinSeries.gammaSet

added def EisensteinSeries.gammaSetEquiv

added theorem EisensteinSeries.gammaSet_one_eq

added def EisensteinSeries.gammaSet_one_equiv

added theorem EisensteinSeries.pairwise_disjoint_gammaSet

added theorem EisensteinSeries.vecMul_SL2_mem_gammaSet

added def eisensteinSeries

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

deleted def ModularForm.eisensteinSeries_MF

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