of_natCast — Mathlib

English

Let α be a type equipped with an additive group with one. For every natural number n, the image of n in α obtained by first embedding n into ZNum and then into α equals n itself.

Русский

Пусть α — множество с аддитивной структурой с единицей. Для каждого натурального числа n образ n в α, полученный через вставку n в ZNum затем в α, равен самому числу n.

LaTeX

$$$\forall n : \mathbb{N}, ((n : ZNum) : \alpha) = n$$$

Lean4

@[simp, norm_cast]
theorem of_natCast [AddGroupWithOne α] (n : ℕ) : ((n : ZNum) : α) = n := by
  rw [← Int.cast_natCast, of_intCast, Int.cast_natCast]

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