decompose_sub — Mathlib

English

Let M be graded by ι with degree components ℳ_i. The decomposition map is additive: for all x,y ∈ M, decompose_ℳ(x − y) = decompose_ℳ(x) − decompose_ℳ(y).

Русский

Пусть M раскладывается по ι с компонентами степени ℳ_i. Разложение является аддитивным: для всех x,y ∈ M имеем decompose_ℳ(x − y) = decompose_ℳ(x) − decompose_ℳ(y).

LaTeX

$$$\operatorname{decompose}_{\mathcal{M}}(x - y) = \operatorname{decompose}_{\mathcal{M}}(x) - \operatorname{decompose}_{\mathcal{M}}(y) \quad( x,y \in M)$$$

Lean4

@[simp]
theorem decompose_sub (x y : M) : decompose ℳ (x - y) = decompose ℳ x - decompose ℳ y :=
  map_sub (decomposeAddEquiv ℳ) x y

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