zero_comp — Mathlib

English

Right composition is additive in the right argument: α . (β₁ + β₂) = α . β₁ + α . β₂.

Русский

Правая композиция по аргументу послего аддитивна: α . (β₁ + β₂) = α . β₁ + α . β₂.

LaTeX

$$$\\alpha. (\\beta_1 + \\beta_2) = (\\alpha.\\beta_1) + (\\alpha.\\beta_2)$$$

Lean4

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

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