coeLinearMap_eq_finsum — Mathlib

English

The canonical linear-map from the weighted submodules to the direct sum coincides with the dfinsupp-sum over coordinates.

Русский

Каноническое линейное отображение совпадает с dfinsupp-суммой по координатам.

LaTeX

$$$(\text{coeLinearMap}\, w)\, x = DFinsupp.sum\, x\, (\lambda\_\_, \; \uparrow\; x)$$$

Lean4

theorem coeLinearMap_eq_finsum [DecidableEq M] (x : DirectSum M fun i : M => ↥(weightedHomogeneousSubmodule R w i)) :
    (DirectSum.coeLinearMap fun i : M => weightedHomogeneousSubmodule R w i) x = finsum fun m => x m := by
  classical
  rw [DirectSum.coeLinearMap_eq_dfinsuppSum, DFinsupp.sum, finsum_eq_sum_of_support_subset]
  apply DirectSum.support_subset

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