leftHomologyMap'_zero — Mathlib

English

If either h1 or h2 is given, the map leftHomologyMap' with zero morphism 0 is zero.

Русский

Если один из объектов данных левой гомологии не задан, отображение leftHomologyMap' от нулевого 0 равно нулю.

LaTeX

$$leftHomologyMap'(0, h_1, h_2) = 0$$

Lean4

@[simp]
theorem leftHomologyMap'_zero (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) : leftHomologyMap' 0 h₁ h₂ = 0 :=
  (LeftHomologyMapData.zero h₁ h₂).leftHomologyMap'_eq

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