Def CuspForm.divDiscriminant

Modification history

2026-05-25 07:57
Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean
feat(NumberTheory/ModularForms): Sturm bound for level-1 modular forms (#38993) …
Modified CuspForm.divDiscriminantView on Github →
2026-05-01 08:23
Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean
feat(NumberTheory/ModularForms): dimension formula for level one modular forms (#37979) …
Added CuspForm.divDiscriminantView on Github →