isZero_homology_of_isZero_X₂ — Mathlib

English

If S.X₂ is zero and S has homology, then S.homology is zero.

Русский

Если X₂ равен нулю и у S есть гомология, то сама гомология равна нулю.

LaTeX

$$IsZero S.X₂ → [S.HasHomology] → IsZero S.homology$$

Lean4

theorem isZero_homology_of_isZero_X₂ (hS : IsZero S.X₂) [S.HasHomology] : IsZero S.homology :=
  IsZero.of_iso hS (HomologyData.ofZeros S (hS.eq_of_tgt _ _) (hS.eq_of_src _ _)).left.homologyIso

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