Commit 2025-09-30 08:44 56610acb

View on Github →

feat(NumberTheory/ModularForms): define modular forms for any subgroup of GL(2, R) (#26651) This PR generalizes (some of) the modular forms files to allow the level to be any subgroup of GL(2, R), not necessarily the image of a subgroup of SL(2, Z). Intended applications include defining Hecke operators.

Estimated changes

modified theorem CuspForm.coe_translate
modified theorem ModularForm.coe_intCast
modified theorem ModularForm.coe_natCast
modified theorem ModularForm.coe_translate
modified def ModularForm.const
modified theorem ModularForm.const_apply
modified def ModularForm.mcast
modified def ModularForm.mul
modified theorem ModularForm.mul_coe
modified theorem ModularForm.one_coe_eq_one
modified theorem SlashInvariantForm.coe_mul