decompose_coe — Mathlib

English

The decomposition is additive: decompose(x+y) = decompose(x) + decompose(y).

Русский

Разложение сохранения сложения: decompose(x+y) = decompose(x) + decompose(y).

LaTeX

$$$\mathrm{decompose}_{\mathcal{M}}(x+y) = \mathrm{decompose}_{\mathcal{M}}(x) + \mathrm{decompose}_{\mathcal{M}}(y)$$$

Lean4

@[simp]
theorem decompose_coe {i : ι} (x : ℳ i) : decompose ℳ (x : M) = DirectSum.of _ i x := by
  rw [← decompose_symm_of _, Equiv.apply_symm_apply]

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