mathlib3

feat(ring_theory/mv_polynomial/symmetric): sum of symmetric polynomials is symmetric

#18640

Open