neg_neg — Mathlib

English

In a non-preadditive abelian category, applying negation twice to a morphism gives the original morphism: −(−a) = a.

Русский

В неабелевой абелиевой категории двойное отрицание возвращает начальный морфизм: −(−a) = a.

LaTeX

$$$ -(-a) = a $$$

Lean4

theorem neg_neg {X Y : C} (a : X ⟶ Y) : - -a = a :=
  by
  rw [neg_def, neg_def]
  conv_lhs => congr; rw [← sub_self a]
  rw [sub_sub_sub, sub_zero, sub_self, sub_zero]

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