cyclesMap'_neg — Mathlib

English

The map leftHomologyMap' is additive with respect to subtraction of morphisms.

Русский

Карта leftHomologyMap' аддитивна по отношению к вычитанию Морфизмов.

LaTeX

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

Lean4

@[simp]
theorem cyclesMap'_neg : cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂ :=
  by
  have γ : LeftHomologyMapData φ h₁ h₂ := default
  simp only [γ.cyclesMap'_eq, γ.neg.cyclesMap'_eq, LeftHomologyMapData.neg_φK]

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