Commit 2023-12-23 00:28 161290d8

View on Github →

feat(ModularForm): Graded Ring instance on spaces of modular forms (#9164) This adds the graded ring instance to spaces of modular forms.

Estimated changes

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

added theorem ModularForm.coe_intCast

added theorem ModularForm.coe_natCast

added def ModularForm.const

added theorem ModularForm.gradedMonoid_eq_of_cast

added def ModularForm.mcast

modified theorem ModularForm.one_coe_eq_one

added theorem ModularForm.toSlashInvariantForm_intCast

added theorem ModularForm.toSlashInvariantForm_natCast

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean

added theorem ModularForm.is_invariant_const

modified theorem ModularForm.is_invariant_one

Modified Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean

added theorem SlashInvariantForm.coe_intCast

added theorem SlashInvariantForm.coe_natCast

added def SlashInvariantForm.const