mathlib

bd4a574f - chore(ring_theory/polynomial/symmetric): golf (#15598)