decompose_symm_neg — Mathlib

English

The inverse map commutes with negation: (decompose ℳ)^{-1}(-x) = −(decompose ℳ)^{-1}(x).

Русский

Обратная к разложению карта коммутирует с отрицанием: decompose^{-1}(-x) = -decompose^{-1}(x).

LaTeX

$$$(\mathrm{decompose}_{\mathcal{M}})^{-1}(-x) = - (\mathrm{decompose}_{\mathcal{M}})^{-1}(x)$$$

Lean4

@[simp]
theorem decompose_symm_neg (x : ⨁ i, ℳ i) : (decompose ℳ).symm (-x) = -(decompose ℳ).symm x :=
  map_neg (decomposeAddEquiv ℳ).symm x

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