Dimension formulas for level-one modular forms

Mathlib (≥ v4.30.0) proves the level-one dimension formulas in Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (ModularForm.dimension_level_one, the rank lemmas for small weights, and CuspForm.discriminantEquiv) and the identity Δ = (E₄³ - E₆²) / 1728 in Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing. Those results are stated for the subgroup 𝒮ℒ; this file transports the ones the project uses to the Γ(1)-indexed spaces used here (CongruenceSubgroup.Gamma_one_coe_eq_SL).

theorem cuspform_weight_lt_12_zero (k : ℤ) (hk : k < 12) : Module.rank ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) = 0

theorem IsCuspForm_weight_lt_eq_zero (k : ℤ) (hk : k < 12) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : IsCuspForm (CongruenceSubgroup.Gamma 1) k f) : f = 0

theorem weight_six_one_dimensional : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6) = 1

theorem weight_four_one_dimensional : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4) = 1

theorem weight_eight_one_dimensional (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (hk3 : k < 12) : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k) = 1

theorem dim_gen_cong_levels (k : ℤ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hΓ : Γ.index ≠ 0) : FiniteDimensional ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)