cast_to_int — Mathlib

English

For any AddGroupWithOne α, the natural embedding of PosNum into α via ℤ equals n, i.e., ((n : ℤ) : α) = n.

Русский

Для любого AddGroupWithOne α естественное вложение PosNum в α через ℤ даёт тот же элемент n: ((n : ℤ) : α) = n.

LaTeX

$$$((n : \\mathbb{Z}) : \\alpha) = n$$$

Lean4

@[simp, norm_cast]
theorem cast_to_int [AddGroupWithOne α] (n : PosNum) : ((n : ℤ) : α) = n := by
  rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]

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