homologyMap'_sub — Mathlib

English

RightHomologyMap' (φ−φ′) = RightHomologyMap'(φ) − RightHomologyMap'(φ′).

Русский

RightHomologyMap'(φ−φ′) = RightHomologyMap'(φ) − RightHomologyMap'(φ′).

LaTeX

$$$\mathrm{rightHomologyMap}'(\varphi-\varphi') = \mathrm{rightHomologyMap}'(\varphi) - \mathrm{rightHomologyMap}'(\varphi')$$$

Lean4

@[simp]
theorem homologyMap'_sub : homologyMap' (φ - φ') h₁ h₂ = homologyMap' φ h₁ h₂ - homologyMap' φ' h₁ h₂ :=
  leftHomologyMap'_sub _ _

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