neg'_add'_self — Mathlib

English

The self-compatibility of addition with neg' holds in the localized setting.

Русский

Совместимость сложения и neg' сохраняется в локализации.

LaTeX

$$$add'\;W\; (neg'\;W\;f)\; f = L.map 0$$$

Lean4

theorem neg'_add'_self (f : L.obj X ⟶ L.obj Y) : add' W (neg' W f) f = L.map 0 :=
  by
  obtain ⟨α, rfl⟩ := exists_leftFraction L W f
  have := inverts L W _ α.hs
  rw [add'_eq W _ _ (LeftFraction₂.mk (-α.f) α.f α.s α.hs) (neg'_eq W _ _ rfl) rfl]
  simp only [← cancel_mono (L.map α.s), LeftFraction.map_comp_map_s, ← L.map_comp, Limits.zero_comp, neg_add_cancel]

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