levelOne_neg_weight_eq_zero — Mathlib

English

If k < 0, then every modular form of weight k is identically zero.

Русский

Если k < 0, то любая модульная форма веса k тождественно равна нулю.

LaTeX

$$$ \forall k \in \mathbb{Z},\ k < 0 \Rightarrow (\forall f \text{ of weight } k,\ f = 0).$$$

Lean4

theorem levelOne_neg_weight_eq_zero (hk : k < 0) (f : F) : ⇑f = 0 :=
  by
  have hf := levelOne_nonpos_wt_const hk.le f
  rcases wt_eq_zero_of_eq_const k hf with rfl | hf₀
  · exact (lt_irrefl _ hk).elim
  · rw [hf, hf₀, const_zero]

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