add_to_nat — Mathlib

English

For all m,n, the Nat cast of m+n equals the Nat cast of m plus the Nat cast of n: ((m+n : Num) : ℕ) = m + n.

Русский

Для всех m,n: преобразование в ℕ после сложения в Num эквивалентно сумме преобразований: ((m+n : Num) : ℕ) = m + n.

LaTeX

$$$\\forall m,n,\\ ((m+n : Num) : \\mathbb{N}) = m + n$$$

Lean4

@[norm_cast]
theorem add_to_nat : ∀ m n, ((m + n : Num) : ℕ) = m + n
  | 0, 0 => rfl
  | 0, pos _q => (Nat.zero_add _).symm
  | pos _p, 0 => rfl
  | pos _p, pos _q => PosNum.add_to_nat _ _

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