Commit 2026-04-24 08:11 5b041439

View on Github →

feat(NumberTheory/ModularForms): cusp form submodule of modular forms (#37978) Introduces the inclusion of cusp forms into modular forms and the corresponding submodule and IsCuspForm predicate. This is in preparation for proving the dimension formula in level one which is in #37979 and see also #37789 The work was done as part of the Sphere packing project. The original code was written by me but the PR was done with the help of Claude Code.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

added def ModularFormClass.modularForm

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

added theorem CongruenceSubgroup.Gamma_one_coe_eq_SL

Created Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean

added def CuspForm.toModularFormₗ

added theorem CuspForm.toModularFormₗ_apply

added theorem CuspForm.toModularFormₗ_eq_coe

added theorem CuspForm.toModularFormₗ_injective

added def ModularForm.CuspForm.equivCuspFormSubmodule

added def ModularForm.IsCuspForm

added def ModularForm.cuspFormSubmodule

added theorem ModularForm.isCuspForm_iff

added theorem ModularForm.isCuspForm_iff_coeffZero_eq_zero

added theorem ModularForm.isZeroAtImInfty_of_valueAtInfty_eq_zero

added theorem ModularForm.isZeroAt_of_coeffZero_eq_zero

added theorem ModularForm.mem_cuspFormSubmodule_iff

added def ModularForm.toCuspForm

added theorem ModularForm.toCuspForm_apply

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

Modified Mathlib/NumberTheory/ModularForms/LevelOne.lean

modified theorem ModularForm.levelOne_weight_zero_rank_one

modified theorem ModularFormClass.levelOne_weight_zero_const

deleted theorem ModularFormClass.one_mem_strictPeriods_SL2Z

added theorem one_mem_strictPeriods_SL

Modified Mathlib/NumberTheory/ModularForms/NormTrace.lean