Commit 2023-03-18 15:37 035e4ef6

View on Github →

feat: port Data.MvPolynomial.CommRing (#2971)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/CommRing.lean

added theorem MvPolynomial.C_neg

added theorem MvPolynomial.C_sub

added theorem MvPolynomial.coeff_neg

added theorem MvPolynomial.coeff_sub

added theorem MvPolynomial.degreeOf_sub_lt

added theorem MvPolynomial.degrees_neg

added theorem MvPolynomial.degrees_sub

added theorem MvPolynomial.eval₂Hom_X

added theorem MvPolynomial.eval₂_neg

added theorem MvPolynomial.eval₂_sub

added def MvPolynomial.homEquiv

added theorem MvPolynomial.hom_C

added theorem MvPolynomial.support_neg

added theorem MvPolynomial.support_sub

added theorem MvPolynomial.totalDegree_neg

added theorem MvPolynomial.totalDegree_sub

added theorem MvPolynomial.vars_neg

added theorem MvPolynomial.vars_sub_of_disjoint

added theorem MvPolynomial.vars_sub_subset