homologyIso_leftHomologyData — Mathlib

English

Equality: S.leftHomologyData.homologyIso equals S.leftHomologyIso inverted.

Русский

Равенство: leftHomologyData.homologyIso равняется обороту leftHomologyIso.

LaTeX

$$$S.leftHomologyData.homologyIso = S.leftHomologyIso^{-1}$$$

Lean4

@[simp]
theorem homologyIso_leftHomologyData [S.HasHomology] : S.leftHomologyData.homologyIso = S.leftHomologyIso.symm :=
  by
  ext
  dsimp [homologyIso, leftHomologyIso, ShortComplex.leftHomologyIso]
  rw [← leftHomologyMap'_comp, comp_id]

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