leftHomologyMap'_sub — Mathlib

English

The additivity of leftHomologyMap' implies its behavior under subtraction of morphisms.

Русский

Аддитивность leftHomologyMap' влечёт поведение при вычитании морфизмов.

LaTeX

$$$ leftHomologyMap'(\varphi - \varphi') = leftHomologyMap'(\varphi) - leftHomologyMap'(\varphi') $$$

Lean4

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

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