coe_natCast — Mathlib

English

For every n ∈ ℕ, the function associated to n via the nat cast equals the constant function n.

Русский

Для каждого n ∈ ℕ соответствующая ему через нат.cast функция равна константе n.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_natCast [Γ.HasDetPlusMinusOne] (n : ℕ) : ⇑(n : SlashInvariantForm Γ 0) = n :=
  rfl

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