cast_one — Mathlib

English

Casting natural n from ℕ into ℤ and then into any AddGroupWithOne R yields the same as the direct cast of n into R.

Русский

Преобразование натурального n через ℤ в R даёт тот же результат, что и прямое преобразование n в R.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem cast_one : ((1 : ℤ) : R) = 1 := by rw [← Int.natCast_one, cast_natCast, Nat.cast_one]

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