const_apply — Mathlib

English

The constant Real-valued modular form maps τ to itsReal value embedded in ℂ.

Русский

Пусть константная вещественная модульная форма отображает τ в свое вещественное значение, как элемент ℂ.

LaTeX

$$$ (\mathrm{const}_{\mathbb{R}}(x))(\tau) = x \in \mathbb{C} \text{ for all } \tau, x \in \mathbb{R}. $$$

Lean4

@[simp]
theorem const_apply [Γ.HasDetOne] (x : ℂ) (τ : ℍ) : (const x : ModularForm Γ 0) τ = x :=
  rfl

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