exactAt_single_obj — Mathlib

English

For each i distinct from j, the complex ((single C c j).obj A) is exact at i.

Русский

Для любого i, отличного от j, комплекс ((single C c j).obj A) является точным в позиции i.

LaTeX

$$$\\mathrm{ExactAt}((\\mathrm{single} C c j).\\mathrm{obj} A) i\\quad(\\text{when } i \\neq j)$$$

Lean4

theorem exactAt_single_obj (A : C) (i : ι) (hi : i ≠ j) : ExactAt ((single C c j).obj A) i :=
  ShortComplex.exact_of_isZero_X₂ _ (isZero_single_obj_X c _ _ _ hi)

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