pure_natCast — Mathlib

English

For any n ∈ ℕ and any α with the required structure, the image of n via the canonical embedding equals the corresponding n in NonemptyInterval α.

Русский

Для любого n ∈ ℕ и любого α с требуемой структурой образ числа n через чистое отображение совпадает с соответствующим элементом в NonemptyInterval α.

LaTeX

$$$\mathrm{pure}(n) = n$$$

Lean4

@[simp]
theorem pure_natCast (n : ℕ) : pure (n : α) = n :=
  rfl

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