exact_iff_isZero_leftHomology — Mathlib

English

For any ShortComplex S with HasHomology, S is exact if and only if its left homology is zero.

Русский

Для любого краткого комплекса S с гомологией S точен тогда и только тогда, когда левая гомология равна нулю.

LaTeX

$$$S.Exact \\iff IsZero S.leftHomology$$$

Lean4

theorem exact_iff_isZero_leftHomology [S.HasHomology] : S.Exact ↔ IsZero S.leftHomology :=
  LeftHomologyData.exact_iff _

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