opcyclesMap'_sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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