cast_ofNat — Mathlib

English

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

Русский

Для любого 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) : ℚ) : α) = (ofNat(n) : α) := by simp [cast_def]

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