levelOne_weight_zero_const — Mathlib

English

If a function f is a modular form of level Γ(1) and weight 0, then f is constant (i.e., its values are all the same scalar). In particular, the space of such forms is spanned by the constant function 1.

Русский

Если функция f является модулярной формой уровня Γ(1) и веса 0, то она константна; пространството таких форм одномерно над ℂ и порождается постоянной функцией 1.

LaTeX

$$$\exists c \in \mathbb{C}, \quad \forall \tau \in \mathbb{H}, \ f(\tau) = c$$$

Lean4

theorem levelOne_weight_zero_const [ModularFormClass F Γ(1) 0] (f : F) : ∃ c, ⇑f = Function.const _ c :=
  ⟨_, levelOne_nonpos_wt_const le_rfl f⟩

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