levelOne_weight_zero_rank_one — Mathlib

English

The space of weight 0 modular forms for level Γ(1) has complex rank 1; it is 1-dimensional over ℂ.

Русский

Пространство модульных форм веса 0 при уровне Γ(1) имеет размерность 1 над ℂ; является одномерным.

LaTeX

$$$\dim_{\mathbb{C}} M_0(\Gamma(1)) = 1$$$

Lean4

theorem levelOne_weight_zero_rank_one : Module.rank ℂ (ModularForm Γ(1) 0) = 1 :=
  by
  refine rank_eq_one (const 1) (by simp [DFunLike.ne_iff]) fun g ↦ ?_
  obtain ⟨c', hc'⟩ := levelOne_weight_zero_const g
  aesop

Похожие утверждения