opcyclesMap'_neg — Mathlib

English

The opcyclesMap' is negated under negation of the morphism.

Русский

opcyclesMap' меняется на противоположное при отрицании морфизма.

LaTeX

$$$ opcyclesMap'(-φ) = - opcyclesMap'(φ) $$$

Lean4

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

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