cast_ofNat — Mathlib

English

For n ∈ ℕ, the cast of ofNat(n) from ℚ≥0 to α equals the corresponding α-embedding: the same numeral in α.

Русский

Для n ∈ ℕ приведение ofNat(n) из ℚ≥0 в α даёт то же представление числа в α.

LaTeX

$$$ (\mathrm{ofNat}(n) : \mathbb{Q}_{\ge 0})^{\uparrow} = (\mathrm{ofNat}(n) : \alpha) $$$

Lean4

@[simp, norm_cast]
theorem cast_ofNat (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : ℚ≥0) = (ofNat(n) : α) :=
  cast_natCast _

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