Commit 2021-01-21 08:15 ce9bc688

View on Github →

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.

Estimated changes

Modified src/data/finset/powerset.lean

added theorem finset.powerset_len_zero

Created src/ring_theory/polynomial/symmetric.lean

added def mv_polynomial.esymm

added theorem mv_polynomial.esymm_eq_sum_monomial

added theorem mv_polynomial.esymm_eq_sum_subtype

added theorem mv_polynomial.esymm_is_symmetric

added theorem mv_polynomial.esymm_zero

added theorem mv_polynomial.is_symmetric.C

added theorem mv_polynomial.is_symmetric.add

added theorem mv_polynomial.is_symmetric.map

added theorem mv_polynomial.is_symmetric.mul

added theorem mv_polynomial.is_symmetric.neg

added theorem mv_polynomial.is_symmetric.one

added theorem mv_polynomial.is_symmetric.smul

added theorem mv_polynomial.is_symmetric.sub

added theorem mv_polynomial.is_symmetric.zero

added def mv_polynomial.is_symmetric

added theorem mv_polynomial.map_esymm

added theorem mv_polynomial.rename_esymm