gradedAlgebra — Mathlib

English

For φ ∈ MvPolynomial σ R and i ∈ ℕ, the i-th component equals homogeneousComponent i φ.

Русский

Для φ ∈ MvPolynomial σ R и i ∈ ℕ, i-я компонентa равна homogeneousComponent i φ.

LaTeX

$$(decomposition.decompose' φ) i = homogeneousComponent i φ$$

Lean4

/-- `MvPolynomial σ R` as a graded algebra, graded by the degree.
We do not make this a global instance because one may want to consider a different
graded algebra structure on `MvPolynomial σ R`, induced by another weight function.
To make it a local instance, you may use
`attribute [local instance] MvPolynomial.gradedAlgebra`.
-/
abbrev gradedAlgebra : GradedAlgebra (homogeneousSubmodule σ R) :=
  weightedGradedAlgebra R (1 : σ → ℕ)

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