cast_to_int — Mathlib

English

For any α with AddGroupWithOne, the two-step cast Num → ℤ → α is the same as interpreting n directly in α: ((n : ℤ) : α) = n.

Русский

Для любой α с AddGroupWithOne композиция Num → ℤ → α даёт то же число: ((n : ℤ) : α) = n.

LaTeX

$$$\\forall {\\alpha} [AddGroupWithOne \\alpha] (n : Num), ((n : \\mathbb{Z}) : \\alpha) = n$$$

Lean4

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

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