English
Let α be any additive monoid with one. The canonical embedding from Num into α preserves addition: for all m, n in Num, the cast of their sum equals the sum of their casts, i.e. ((m + n) : α) = m + n.
Русский
Пусть α — моноид аддитивной структуры с единицей. Приведение из Num в α сохраняет сложение: для всех m, n ∈ Num выполняется ((m + n) : α) = m + n, где правая сумма берется в α.
LaTeX
$$$((m + n :
Num) : \alpha) = m + n$$$
Lean4
@[simp, norm_cast]
theorem cast_add [AddMonoidWithOne α] (m n) : ((m + n : Num) : α) = m + n := by
rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]
