Def ModularForm.const

Modification history

2025-12-07 16:03

Mathlib/NumberTheory/ModularForms/Basic.lean

feat(ModularForms): norm and trace maps (#32460) …

Modified ModularForm.const View on Github →

2025-09-30 08:44

Mathlib/NumberTheory/ModularForms/Basic.lean

feat(NumberTheory/ModularForms): define modular forms for any subgroup of GL(2, R) (#26651) …

Modified ModularForm.const View on Github →

2023-12-23 00:28

Mathlib/NumberTheory/ModularForms/Basic.lean

feat(ModularForm): Graded Ring instance on spaces of modular forms (#9164) …

Added ModularForm.const View on Github →