mathlib3

ce9bc688 - feat(ring_theory/polynomial): symmetric polynomials and elementary symmetric polynomials (#5788)

feat(ring_theory/polynomial): symmetric polynomials and elementary symmetric polynomials (#5788) Define symmetric polynomials and elementary symmetric polynomials, and prove some basic facts about them.