weightedHomogeneousComponent — Mathlib

English

Reiterates that weighted homogeneous submodules form a graded monoid with unit in degree 0 and multiplication consistent with degree addition.

Русский

Повторяет, что взвешенно однородные подмодули образуют градиентный моноид с единицей в степени 0 и умножение согласовано с суммой степеней.

LaTeX

$$SetLike.GradedMonoid (weightedHomogeneousSubmodule R w)$$

Lean4

/-- `weightedHomogeneousComponent w n φ` is the part of `φ` that is weighted homogeneous of
  weighted degree `n`, with respect to the weights `w`.
  See `sum_weightedHomogeneousComponent` for the statement that `φ` is equal to the sum
  of all its weighted homogeneous components. -/
def weightedHomogeneousComponent (w : σ → M) (n : M) : MvPolynomial σ R →ₗ[R] MvPolynomial σ R :=
  letI := Classical.decEq M
  (Submodule.subtype _).comp <| Finsupp.restrictDom _ _ {d | weight w d = n}

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