isIso_cyclesMap'_of_isIso — Mathlib

English

If φ is an isomorphism, then cyclesMap' φ h1 h2 is an isomorphism.

Русский

Если φ — изоморфизм, то cyclesMap' φ h1 h2 является изоморфизмом.

LaTeX

$$IsIso (cyclesMap'(\phi,h_1,h_2))$$

Lean4

instance isIso_cyclesMap'_of_isIso (φ : S₁ ⟶ S₂) [IsIso φ] (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    IsIso (cyclesMap' φ h₁ h₂) :=
  (inferInstance : IsIso (cyclesMapIso' (asIso φ) h₁ h₂).hom)

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