English
For a given φ in the multivariate polynomial ring and weight w, the weighted decomposition decompose' coincides with DirectSum.mk over the weights appearing in the support of φ, assigning to each weight m the component weightedHomogeneousComponent w m φ.
Русский
Для данного φ ∈ многопеременного полинома и веса w разложение по весам decompose' совпадает с DirectSum.mk по весам, встречающимся в опорном наборе φ, где для каждого веса m даётся компонент weightedHomogeneousComponent w m φ.
LaTeX
$$$(\\text{weightedDecomposition } R w).decompose' (\\phi) = \\mathrm{DirectSum.mk}\\big(\\cdots\\big)\\;,$$$
Lean4
theorem decompose'_eq [DecidableEq M] :
(weightedDecomposition R w).decompose' = fun φ : MvPolynomial σ R =>
DirectSum.mk (fun i : M => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (weight w) φ.support) fun m =>
⟨weightedHomogeneousComponent w m φ, weightedHomogeneousComponent_mem w φ m⟩ :=
rfl
