cast_add — Mathlib

English

Let m,n be elements of ZNum. The embedding into α preserves addition: the image of m+n equals the sum of the images.

Русский

Пусть m,n принадлежат ZNum. Встраивание в α сохраняет сложение: образ m+n равен сумме образов m и n.

LaTeX

$$$$\forall m,n \in ZNum,\ ((m+n : ZNum) : α) = (m : α) + (n : α).$$$$

Lean4

@[simp, norm_cast]
theorem cast_add [AddGroupWithOne α] : ∀ m n, ((m + n : ZNum) : α) = m + n
  | 0, a => by cases a <;> exact (_root_.zero_add _).symm
  | b, 0 => by cases b <;> exact (_root_.add_zero _).symm
  | pos _, pos _ => PosNum.cast_add _ _
  | pos a, neg b => by simpa only [sub_eq_add_neg] using PosNum.cast_sub' (α := α) _ _
  | neg a, pos b =>
    have : (↑b + -↑a : α) = -↑a + ↑b :=
      by
      rw [← PosNum.cast_to_int a, ← PosNum.cast_to_int b, ← Int.cast_neg, ← Int.cast_add (-a)]
      simp [add_comm]
    (PosNum.cast_sub' _ _).trans <| (sub_eq_add_neg _ _).trans this
  | neg a, neg b =>
    show -(↑(a + b) : α) = -a + -b by
      rw [PosNum.cast_add, neg_eq_iff_eq_neg, neg_add_rev, neg_neg, neg_neg, ← PosNum.cast_to_int a, ←
        PosNum.cast_to_int b, ← Int.cast_add, ← Int.cast_add, add_comm]

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