coeAddMonoidHom_eq_support_sum — Mathlib

English

In the direct-sum decomposition of a polynomial into weighted homogeneous components, the m-th component of the image under the direct-sum embedding equals the m-th coordinate of the direct sum.

Русский

В разложении через прямую сумму компонент полинома совпадает с соответствующей координатой прямой суммы.

LaTeX

$$$weightedHomogeneousComponent\, w\, m\, (DirectSum.coeLinearMap\, R\, w\, x) = x\, m$$$

Lean4

theorem coeAddMonoidHom_eq_support_sum [DecidableEq σ] [DecidableEq R] [DecidableEq M]
    (x : DirectSum M fun i : M => ↥(weightedHomogeneousSubmodule R w i)) :
    (DirectSum.coeAddMonoidHom fun i : M => weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x (fun _ x => ↑x) :=
  DirectSum.coeLinearMap_eq_dfinsuppSum R w x

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