Def CuspForm.ofMulDiscriminant

Modification history

2026-05-01 08:23

Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean

feat(NumberTheory/ModularForms): dimension formula for level one modular forms (#37979) …

Added CuspForm.ofMulDiscriminant View on Github →