decompose'_apply — Mathlib

English

The decomposition' equals the explicit direct-sum construction that collects each degree i part with its witness homogeneousComponent i φ.

Русский

Разложение' равно явному конструкту прямой суммы, собирающему каждую часть степени i с её компонентой homogenеousComponent i φ.

LaTeX

$$decomposition.decompose' = fun φ => DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (φ.support.image Finsupp.degree) (fun m => ⟨homogeneousComponent m φ, homogeneousComponent_mem m φ⟩)$$

Lean4

theorem decompose'_apply (φ : MvPolynomial σ R) (i : ℕ) :
    (decomposition.decompose' φ i : MvPolynomial σ R) = homogeneousComponent i φ :=
  weightedDecomposition.decompose'_apply R _ φ i

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