constℝ_apply — Mathlib

English

The constant real-valued modular form with x ∈ ℝ yields a modular form of weight 0.

Русский

Постоянная вещественная модульная форма с значением x ∈ ℝ задает модульную форму веса 0.

LaTeX

$$$ (\mathrm{const}_{\mathbb{R}}(x))(z) = x, \; x \in \mathbb{R}. $$$

Lean4

@[simp]
theorem constℝ_apply [Γ.HasDetPlusMinusOne] (x : ℝ) (τ : ℍ) : (constℝ x : ModularForm Γ 0) τ = x :=
  rfl

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