comp_neg — Mathlib

English

Composition with a negated right factor equals the negation of the composition: α . (-β) = -(α . β).

Русский

Композиция слева с отрицанием справа равна отрицанию самой композиции: α . (-β) = -(α . β).

LaTeX

$$$\\alpha.(-\\beta) = -(\\alpha.\\beta)$$$

Lean4

@[simp]
theorem comp_neg (α : Ext X Y n) {m : ℕ} (β : Ext Y Z m) {p : ℕ} (h : n + m = p) : α.comp (-β) h = -α.comp β h := by
  letI := HasDerivedCategory.standard C; ext; simp [this, neg_hom']

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