coe_intCast — Mathlib

English

Same as above: integer cast yields the constant function equal to that integer.

Русский

То же: целочисленный каст даёт константную функцию, равную этому целому числу.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_intCast [Γ.HasDetPlusMinusOne] (z : ℤ) : ⇑(z : SlashInvariantForm Γ 0) = z :=
  rfl

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