of_natCast — Mathlib

English

For any α with AddMonoidWithOne, the numeral n in Num corresponds to n in α: ((n : Num) : α) = n.

Русский

Для любого α с AddMonoidWithOne числительное n в Num соответствует n в α: ((n : Num) : α) = n.

LaTeX

$$$\\forall {\\alpha} [AddMonoidWithOne \\alpha] (n : ℕ), ((n : Num) : \\alpha) = n$$$

Lean4

@[simp, norm_cast]
theorem of_natCast {α} [AddMonoidWithOne α] (n : ℕ) : ((n : Num) : α) = n := by rw [← cast_to_nat, to_of_nat]

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