mathlib

dad5aabe - refactor(ring_theory/polynomial/homogeneous): redefine `mv_polynomial.homogeneous_component` (#5294)

refactor(ring_theory/polynomial/homogeneous): redefine `mv_polynomial.homogeneous_component` (#5294) * redefine `homogeneous_component` using `finsupp.restrict_dom`, “upgrade” it to a `linear_map`; * add `coeff_homogeneous_component` and use it to golf some proofs.