Theorem ModularForm.one_coe_eq_one

Modification history

2023-12-23 00:28

Mathlib/NumberTheory/ModularForms/Basic.lean

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

Modified ModularForm.one_coe_eq_one View on Github →

2023-07-03 16:47

Mathlib/NumberTheory/ModularForms/Basic.lean

feat: port NumberTheory.ModularForms.Basic (#5662)

Added ModularForm.one_coe_eq_one View on Github →