eq_zero — Mathlib

English

In a HomOrthogonal family with HasZeroMorphisms, a morphism between non-adjacent summands is zero.

Русский

При наличии нулевых морфизмов и гомортогональности между непохожими слагаемыми равенство нулю.

LaTeX

$$$$f=0\\;\\text{when } f: s_i \\to s_j\\text{ with } i\\neq j.$$$$

Lean4

theorem eq_zero [HasZeroMorphisms C] (o : HomOrthogonal s) {i j : ι} (w : i ≠ j) (f : s i ⟶ s j) : f = 0 :=
  (o w).elim _ _

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