decomposition — Mathlib

English

The decomposition maps MvPolynomial σ R onto the direct sum of homogeneous submodules: MvPolynomial σ R ≅ ⨁_i homogeneousSubmodule σ R i.

Русский

Разложение MvPolynomial σ R по прямой сумме однородных подмодулей: MvPolynomial σ R ≅ ⨁_i homogeneousSubmodule σ R i.

LaTeX

$$decomposition : DirectSum.Decomposition (homogeneousSubmodule σ R)$$

Lean4

/-- The decomposition of `MvPolynomial σ R` into homogeneous submodules. -/
abbrev decomposition : DirectSum.Decomposition (homogeneousSubmodule σ R) :=
  weightedDecomposition R (1 : σ → ℕ)

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