rightHomologyMap'_sub — Mathlib

English

For φ, φ′ with right homology data h1,h2, the map rightHomologyMap' is additive with subtraction: rightHomologyMap'(φ−φ') h1 h2 = rightHomologyMap'(φ) h1 h2 − rightHomologyMap'(φ') h1 h2.

Русский

Для φ, φ′ с данными правой гомологии h1,h2 отображение rightHomologyMap' аддитивно по вычитанию: rightHomologyMap'(φ−φ') h1 h2 = rightHomologyMap'(φ) h1 h2 − rightHomologyMap'(φ') h1 h2.

LaTeX

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

Lean4

@[simp]
theorem rightHomologyMap'_sub :
    rightHomologyMap' (φ - φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ - rightHomologyMap' φ' h₁ h₂ := by
  simp only [sub_eq_add_neg, rightHomologyMap'_add, rightHomologyMap'_neg]

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