coeLinearMap_eq_dfinsuppSum — Mathlib

English

The value of the canonical linear map on an element x of the direct sum equals the sum over i of the coordinate x_i viewed in A_i.

Русский

Значение канонического линейного отображения на элементе x прямой суммы равно сумме координат x_i, взятых в A_i.

LaTeX

$$$\mathrm{coeLinearMap} A\; x = \mathrm{DFinsupp}.sum\ x\ (\\lambda i x \!:\! A_i, \; x).$$$

Lean4

theorem coeLinearMap_eq_dfinsuppSum [DecidableEq M] (x : DirectSum ι fun i => A i) :
    coeLinearMap A x = DFinsupp.sum x fun i => (fun x : A i => ↑x) :=
  by
  simp only [coeLinearMap, toModule, DFinsupp.lsum, LinearEquiv.coe_mk, LinearMap.coe_mk, AddHom.coe_mk]
  rw [DFinsupp.sumAddHom_apply]
  simp only [LinearMap.toAddMonoidHom_coe, Submodule.coe_subtype]

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