decompose_smul — Mathlib

English

The decomposition map commutes with scalar multiplication: decompose ℳ (r · x) = r · decompose ℳ x for r ∈ R, x ∈ M.

Русский

Разложение командует по умножению на скаляр: decompose_ℳ(r·x) = r·decompose_ℳ(x).

LaTeX

$$$\operatorname{decompose}_{\mathcal{M}}(r\cdot x) = r\cdot \operatorname{decompose}_{\mathcal{M}}(x)$$$

Lean4

@[simp]
theorem decompose_smul (r : R) (x : M) : decompose ℳ (r • x) = r • decompose ℳ x :=
  map_smul (decomposeLinearEquiv ℳ) r x

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