cast_ofNat — Mathlib

English

For any Nat n with the usual AtLeastTwo condition, the cast of ofNat n from ℤ to R equals ofNat n.

Русский

Для любого натурального n с учётом условия AtLeastTwo отображение from ℤ к R через ofNat возвращает того же значения.

LaTeX

$$$((\mathrm{ofNat}(n) : \mathbb{Z}) : R) = \mathrm{ofNat}(n)$$$

Lean4

@[simp, norm_cast]
theorem cast_ofNat (n : ℕ) [n.AtLeastTwo] : ((ofNat(n) : ℤ) : R) = ofNat(n) := by
  simpa only [OfNat.ofNat] using AddGroupWithOne.intCast_ofNat (R := R) n

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