comp_distTriang_mor_zero₃₁ — Mathlib

English

In a distinguished triangle, the composition of the first two morphisms is zero.

Русский

В выделенном треугольнике композиция первых двух морфизмов равна нулю.

LaTeX

$$comp_distTriang_mor_zero₁₂$$

Lean4

/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `h ≫ f⟦1⟧ = 0`. -/
@[reassoc, stacks 0146]
theorem comp_distTriang_mor_zero₃₁ (T : Triangle C) (H : T ∈ distTriang C) : T.mor₃ ≫ T.mor₁⟦1⟧' = 0 :=
  by
  have H₂ := rot_of_distTriang T.rotate (rot_of_distTriang T H)
  simpa using comp_distTriang_mor_zero₁₂ T.rotate.rotate H₂

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