Theorems · Definition · commutative algebra

MvPolynomial.weightedHomogeneousComponent

{R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → {σ : Type u_3} → [AddCommMonoid M] → (σ → M) → M → MvPolynomial σ R →ₗ[R] MvPolynomial σ R

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.

Defined in

Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Cited by

25 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoid