Theorem ModularForm.mul_coe

Modification history

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.mul_coe View on Github →

2023-07-03 16:47

Mathlib/NumberTheory/ModularForms/Basic.lean

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

Added ModularForm.mul_coe View on Github →