coeHom — Mathlib

English

There is a canonical additive map from ModularForm Γ k to the space of functions on the upper half-plane, defined by f ↦ (τ ↦ f(τ)).

Русский

Существует каноническое аддитивное отображение из ModularForm Γ k в пространство функций на верхней полуплоскости, генерируемое f ↦ (τ ↦ f(τ)).

LaTeX

$$$ \mathrm{coeHom}(f)(\tau) = f(\tau) \quad \text{for all } \tau \in \mathbb{H}. $$$

Lean4

/-- Additive coercion from `ModularForm` to `ℍ → ℂ`. -/
@[simps]
def coeHom : ModularForm Γ k →+ ℍ → ℂ where
  toFun f := f
  map_zero' := coe_zero
  map_add' _ _ := rfl

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