add_comm — Mathlib

English

For any morphisms a, b: X → Y in an abelian non-preadditive context, a + b = b + a.

Русский

Пусть a, b: X ⟶ Y. Тогда a + b = b + a.

LaTeX

$$$ a + b = b + a $$$

Lean4

theorem add_comm {X Y : C} (a b : X ⟶ Y) : a + b = b + a :=
  by
  rw [add_def]
  conv_lhs => rw [← neg_neg a]
  rw [neg_def, neg_def, neg_def, sub_sub_sub]
  conv_lhs =>
    congr
    next => skip
    rw [← neg_def, neg_sub]
  rw [sub_sub_sub, add_def, ← neg_def, neg_neg b, neg_def]

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