Commit 2023-08-15 04:44 63ae2f41

View on Github →

feat(RingTheory/MvPolynomial/NewtonIdentities): Add proof of Newton's identities (#6139)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fintype/Powerset.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

Created Mathlib/RingTheory/MvPolynomial/NewtonIdentities.lean

added theorem MvPolynomial.mul_esymm_eq_sum

added theorem MvPolynomial.psum_eq_mul_esymm_sub_sum

added theorem MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero

Modified Mathlib/RingTheory/MvPolynomial/Symmetric.lean

added def MvPolynomial.psum

added theorem MvPolynomial.psum_def

added theorem MvPolynomial.psum_isSymmetric

added theorem MvPolynomial.psum_one

added theorem MvPolynomial.psum_zero

added theorem MvPolynomial.rename_psum

Modified docs/references.bib

Modified docs/undergrad.yaml