Theorem ModularForm.discriminant_bounded_factor

Modification history

2026-05-01 08:23
Mathlib/NumberTheory/ModularForms/Discriminant.lean
feat(NumberTheory/ModularForms): dimension formula for level one modular forms (#37979) …
Deleted ModularForm.discriminant_bounded_factorView on Github →
2026-03-31 07:42
Mathlib/NumberTheory/ModularForms/Discriminant.lean
feat(NumberTheory/ModularForms): modular discriminant as a cusp form (#36262) …
Added ModularForm.discriminant_bounded_factorView on Github →