instIntCastOfNatIntOfHasDetPlusMinusOneFinNatReal

English

For every z ∈ ℤ, the function associated to z via the int cast equals the constant function z.

Русский

Для каждого z ∈ ℤ соответствующая ему функция через целочисленный каст равна константе z.

LaTeX

$$$\forall z\in\mathbb{Z},\ (z:\mathrm{SlashInvariantForm}(\Gamma,0))(\tau)=z\quad\forall \tau\in\mathbb{H}. $$$

Lean4

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

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