instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal

English

For Γ with det ±1, the integer cast of any z ∈ ℤ to a modular form of weight 0 is the constant function equal to z.

Русский

Пусть Γ с det ±1. Целочисленное отображение z ∈ ℤ в модулярную форму веса 0 является константной функцией, равной z.

LaTeX

$$$\forall {\Gamma} [\GammaHasDetPlusMinusOne] (z : \mathbb{Z}):\forall t \in \mathbb{H}, ((z : \mathrm{ModularForm}(\Gamma,0)))(t) = z.$$$

Lean4

instance [Γ.HasDetPlusMinusOne] : IntCast (ModularForm Γ 0) where intCast z := constℝ z

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