cast_add — Mathlib

English

For all m, n ∈ ℕ, the cast of m + n equals the sum of the casts: (m + n) cast = m cast + n cast.

Русский

Для любых m, n ∈ ℕ приведение суммы к R равняется сумме приведений: (m + n) cast = m cast + n cast.

LaTeX

$$$ (m + n)^{\uparrow} = m^{\uparrow} + n^{\uparrow} $$$

Lean4

@[simp, norm_cast]
theorem cast_add [AddMonoidWithOne R] (m n : ℕ) : ((m + n : ℕ) : R) = m + n := by
  induction n with
  | zero => simp
  | succ n ih => rw [add_succ, cast_succ, ih, cast_succ, add_assoc]

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