hasRightHomology_iff_op — Mathlib

English

A ShortComplex S has right homology if and only if its opposite has left homology.

Русский

Короткий комплекс S имеет правую гомологию тогда и только тогда, когда его противоположность имеет левую гомологию.

LaTeX

$$$ HasRightHomology(S) \iff HasLeftHomology(S^{op}) $$$

Lean4

theorem hasRightHomology_iff_op (S : ShortComplex C) : S.HasRightHomology ↔ S.op.HasLeftHomology :=
  ⟨fun _ => inferInstance, fun _ => HasRightHomology.mk' S.op.leftHomologyData.unop⟩

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