Theorem CuspForm.exists_smul_discriminant_of_weight_eq_twelve

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