Commit 2023-03-29 06:00 bcbee715

feat(ring_theory/mv_polynomial/weighted homogeneous): add weighted homogeneous polynomials (#17855) It is possible to assign weights (in a commutative additive monoid M) to the variables of a multivariate polynomial ring, so that monomials of the ring then have a weighted degree with respect to the weights of the variables. The weights are represented by a function w : σ → M, where σ are the indeterminates. A multivariate polynomial φ is weighted homogeneous of weighted degree m : M if all monomials occuring in φ have the same weighted degree m.