English
For the symmetrized decomposition, (decompose ℳ).symm preserves subtraction: (decompose ℳ).symm (x − y) = (decompose ℳ).symm x − (decompose ℳ).symm y for x,y in the direct sum.
Русский
Для симметризированного разложения выполняется сохранение вычитания: (decompose ℳ).symm (x − y) = (decompose ℳ).symm x − (decompose ℳ).symm y для элементов x,y прямой суммы.
LaTeX
$$$\big((\operatorname{decompose}_{\mathcal{M}})^{\mathrm{symm}}\big)(x - y) = \big((\operatorname{decompose}_{\mathcal{M}})^{\mathrm{symm}}\big)x - \big((\operatorname{decompose}_{\mathcal{M}})^{\mathrm{symm}}\big)y$$$
Lean4
@[simp]
theorem decompose_symm_sub (x y : ⨁ i, ℳ i) :
(decompose ℳ).symm (x - y) = (decompose ℳ).symm x - (decompose ℳ).symm y :=
map_sub (decomposeAddEquiv ℳ).symm x y
