mathlib

83b0981b - feat(ring_theory/polynomial): the symmetric and homogenous polynomials form a subalgebra and submodules, respectively (#6666)

feat(ring_theory/polynomial): the symmetric and homogenous polynomials form a subalgebra and submodules, respectively (#6666) This adds: * the new definitions: * `mv_polynomial.homogeneous_submodule σ R n`, defined as the `{ x | x.is_homogeneous n }` * `mv_polynomial.symmetric_subalgebra σ R`, defined as the `{ x | x.is_symmetric }` * simp lemmas to reduce membership of the above to the `.is_*` form * `mv_polynomial.homogenous_submodule_mul` a statement about the product of homogenous submodules * `mv_polynomial.homogenous_submodule_eq_finsupp_supported` a statement that we already have a different definition of homogenous submodules elsewhere All the other proofs have just been moved around the files.