rightHomologyMap'_zero — Mathlib

English

The zero morphism between.RightHomologyData is sent to the zero morphism by rightHomologyMap'.

Русский

Нулевой морфизм между RightHomologyData отображается в нулевой морфизм RightHomologyMap'.

LaTeX

$$rightHomologyMap' 0 h₁ h₂ = 0$$

Lean4

@[simp]
theorem rightHomologyMap'_zero (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    rightHomologyMap' 0 h₁ h₂ = 0 :=
  (RightHomologyMapData.zero h₁ h₂).rightHomologyMap'_eq

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