Commit 2024-08-04 10:22 240d6edb

View on Github →

feat: Complete homogeneous and monomial symmetric polynomials (#12572) Implement complete homogeneous and monomial symmetric polynomials.

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric.lean

modified theorem MvPolynomial.aeval_esymm_eq_multiset_esymm

modified theorem MvPolynomial.degrees_esymm

added def MvPolynomial.esymmPart

added theorem MvPolynomial.esymmPart_indiscrete

added theorem MvPolynomial.esymmPart_zero

added theorem MvPolynomial.esymm_one

added def MvPolynomial.hsymm

added def MvPolynomial.hsymmPart

added theorem MvPolynomial.hsymmPart_indiscrete

added theorem MvPolynomial.hsymmPart_zero

added theorem MvPolynomial.hsymm_isSymmetric

added theorem MvPolynomial.hsymm_one

added theorem MvPolynomial.hsymm_zero

added theorem MvPolynomial.map_hsymm

added def MvPolynomial.msymm

added theorem MvPolynomial.msymm_isSymmetric

added theorem MvPolynomial.msymm_one

added theorem MvPolynomial.msymm_zero

added def MvPolynomial.psumPart

added theorem MvPolynomial.psumPart_indiscrete

added theorem MvPolynomial.psumPart_zero

deleted theorem MvPolynomial.psum_def

modified theorem MvPolynomial.psum_one

modified theorem MvPolynomial.psum_zero

added theorem MvPolynomial.rename_hsymm

added theorem MvPolynomial.rename_msymm

modified theorem MvPolynomial.support_esymm''

modified theorem MvPolynomial.support_esymm'

modified theorem MvPolynomial.support_esymm

modified def MvPolynomial.symmetricSubalgebra