levelOne_neg_weight_rank_zero — Mathlib

English

If the weight k is negative, the space of modular forms of weight k for level Γ(1) is zero-dimensional (only the zero form).

Русский

Если вес k отрицателен, пространство модульных форм веса k при уровне Γ(1) тривиально: состоит только из нулевой формы.

LaTeX

$$$\text{If } k < 0,\quad \dim_{\mathbb{C}} M_k(\Gamma(1)) = 0.$$$

Lean4

theorem levelOne_neg_weight_rank_zero (hk : k < 0) : Module.rank ℂ (ModularForm Γ(1) k) = 0 :=
  by
  refine rank_eq_zero_iff.mpr fun f ↦ ⟨_, one_ne_zero, ?_⟩
  simpa only [one_smul, ← DFunLike.coe_injective.eq_iff] using levelOne_neg_weight_eq_zero hk f

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