cast_add — Mathlib

English

The embedding preserves addition: for m,n in PosNum, cast((m+n)) = cast(m) + cast(n).

Русский

Встраивание сохраняет сложение: для m,n ∈ PosNum, cast(m+n) = cast(m) + cast(n).

LaTeX

$$$[AddMonoidWithOne \\alpha] (m,n) : ((m + n) : \\alpha) = m + n$$$

Lean4

@[simp, norm_cast]
theorem cast_add [AddMonoidWithOne α] (m n) : ((m + n : PosNum) : α) = m + n := by
  rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]

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