mathlib3

bcbee715 - feat(ring_theory/mv_polynomial/weighted homogeneous): add weighted homogeneous polynomials (#17855)

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`. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>