Commit 2025-08-28 10:52 bbe8c9ac

View on Github →

feat(NumberTheory/ModularForms/EisensteinSeries): Update gammaSet (#27840) We redefine gammaSet to include vectors with non-trivial gcd. This is useful for giving the q-expansions of Eisenstein series at level one. Which can be seen here #27606 (these equivalences are used in tsum_prod_eisSummand_eq_riemannZeta_eisensteinSeries in the QExpansions file).

Estimated changes

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

added theorem EisensteinSeries.finGcdMap_div

added theorem EisensteinSeries.finGcdMap_smul

modified def EisensteinSeries.gammaSet

added def EisensteinSeries.gammaSetDivGcdEquiv

added def EisensteinSeries.gammaSetDivGcdSigmaEquiv

added theorem EisensteinSeries.gammaSetDivGcdSigmaEquiv_symm_eq

modified def EisensteinSeries.gammaSetEquiv

added theorem EisensteinSeries.gammaSet_div_gcd

added theorem EisensteinSeries.gammaSet_div_gcd_to_gammaSet10_bijection

added theorem EisensteinSeries.gammaSet_eq_gcd_mul_divIntMap

added theorem EisensteinSeries.gammaSet_one_const

modified theorem EisensteinSeries.gammaSet_one_eq

modified def EisensteinSeries.gammaSet_one_equiv

added theorem EisensteinSeries.gammaSet_one_mem_iff

added theorem EisensteinSeries.mem_gammaSet_one

modified theorem EisensteinSeries.pairwise_disjoint_gammaSet

added theorem EisensteinSeries.vecMulSL_gcd

modified theorem EisensteinSeries.vecMul_SL2_mem_gammaSet

modified def eisensteinSeries

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

Modified Mathlib/RingTheory/EuclideanDomain.lean

added theorem isCoprime_div_gcd_div_gcd_of_gcd_ne_zero