cyclesMap'_sub — Mathlib

English

CyclesMap respects subtraction: cyclesMap(φ − φ') = cyclesMap φ − cyclesMap φ'.

Русский

CyclesMap сохраняет вычитание: cyclesMap(φ − φ') = cyclesMap φ − cyclesMap φ'.

LaTeX

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

Lean4

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

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