cast_natCast — Mathlib

English

For any natural n, the embedding coincides with the usual embedding of n into α: ((n : ℚ≥0) : α) = n.

Русский

Для любого натурального числа n вложение совпадает с обычным вложением числа n в α: ((n : ℚ≥0) : α) = n.

LaTeX

$$$ (n : \mathbb{Q}_{\ge 0})^{\uparrow} = n $ in α, (n \in \mathbb{N})$$

Lean4

@[simp, norm_cast]
theorem cast_natCast (n : ℕ) : ((n : ℚ≥0) : α) = n := by simp [cast_def]

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