Commit 2024-01-19 11:22 e29e9b5c

View on Github →

feat: add definition of Eisenstein series (#9783) This defines Eisenstein series of level N and shows that they are a slash invariant form. Also adds some pre-requisites for proving they are modular forms, which will be in the next PRs

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

added theorem IsCoprime.exists_SL2_col

added theorem IsCoprime.exists_SL2_row

added theorem IsCoprime.mulVecSL

added theorem IsCoprime.vecMulSL

added theorem Matrix.SpecialLinearGroup.coe_transpose

added theorem Matrix.SpecialLinearGroup.isCoprime_col

added theorem Matrix.SpecialLinearGroup.isCoprime_row

added def Matrix.SpecialLinearGroup.transpose

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

added def EisensteinSeries.eisSummand

added theorem EisensteinSeries.eisSummand_SL2_apply

added def EisensteinSeries.eisensteinSeries

added def EisensteinSeries.eisensteinSeries_SIF

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