Commit 2023-03-19 06:37 0989d4a8

View on Github →

feat: port RingTheory.MvPolynomial.Symmetric (#2981)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/MvPolynomial/Symmetric.lean

added theorem Multiset.Finset.esymm_map_val

added def Multiset.esymm

added theorem MvPolynomial.IsSymmetric.add

added theorem MvPolynomial.IsSymmetric.c

added theorem MvPolynomial.IsSymmetric.map

added theorem MvPolynomial.IsSymmetric.mul

added theorem MvPolynomial.IsSymmetric.neg

added theorem MvPolynomial.IsSymmetric.one

added theorem MvPolynomial.IsSymmetric.smul

added theorem MvPolynomial.IsSymmetric.sub

added theorem MvPolynomial.IsSymmetric.zero

added def MvPolynomial.IsSymmetric

added theorem MvPolynomial.aeval_esymm_eq_multiset_esymm

added theorem MvPolynomial.degrees_esymm

added def MvPolynomial.esymm

added theorem MvPolynomial.esymm_eq_multiset_esymm

added theorem MvPolynomial.esymm_eq_sum_monomial

added theorem MvPolynomial.esymm_eq_sum_subtype

added theorem MvPolynomial.esymm_isSymmetric

added theorem MvPolynomial.esymm_zero

added theorem MvPolynomial.map_esymm

added theorem MvPolynomial.mem_symmetricSubalgebra

added theorem MvPolynomial.rename_esymm

added theorem MvPolynomial.support_esymm''

added theorem MvPolynomial.support_esymm'

added theorem MvPolynomial.support_esymm

added def MvPolynomial.symmetricSubalgebra