Commit 2023-03-24 16:57 45092e11

View on Github →

feat: port Data.MvPolynomial.Equiv (#2997)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Equiv.lean

added theorem MvPolynomial.coeff_eval_eq_eval_coeff

added theorem MvPolynomial.degreeOf_coeff_finSuccEquiv

added theorem MvPolynomial.degree_finSuccEquiv

added theorem MvPolynomial.eval_eq_eval_mv_eval'

added def MvPolynomial.finSuccEquiv

added theorem MvPolynomial.finSuccEquiv_X_succ

added theorem MvPolynomial.finSuccEquiv_X_zero

added theorem MvPolynomial.finSuccEquiv_apply

added theorem MvPolynomial.finSuccEquiv_coeff_coeff

added theorem MvPolynomial.finSuccEquiv_comp_C_eq_C

added theorem MvPolynomial.finSuccEquiv_eq

added theorem MvPolynomial.finSuccEquiv_support'

added theorem MvPolynomial.finSuccEquiv_support

added def MvPolynomial.isEmptyAlgEquiv

added def MvPolynomial.isEmptyRingEquiv

added def MvPolynomial.iterToSum

added theorem MvPolynomial.iterToSum_C_C

added theorem MvPolynomial.iterToSum_C_X

added theorem MvPolynomial.iterToSum_X

added def MvPolynomial.mapAlgEquiv

added theorem MvPolynomial.mapAlgEquiv_refl

added theorem MvPolynomial.mapAlgEquiv_symm

added theorem MvPolynomial.mapAlgEquiv_trans

added def MvPolynomial.mapEquiv

added theorem MvPolynomial.mapEquiv_refl

added theorem MvPolynomial.mapEquiv_symm

added theorem MvPolynomial.mapEquiv_trans

added def MvPolynomial.mvPolynomialEquivMvPolynomial

added theorem MvPolynomial.natDegree_finSuccEquiv

added def MvPolynomial.optionEquivLeft

added def MvPolynomial.optionEquivRight

added def MvPolynomial.pUnitAlgEquiv

added def MvPolynomial.sumAlgEquiv

added def MvPolynomial.sumRingEquiv

added def MvPolynomial.sumToIter

added theorem MvPolynomial.sumToIter_C

added theorem MvPolynomial.sumToIter_Xl

added theorem MvPolynomial.sumToIter_Xr

added theorem MvPolynomial.support_coeff_finSuccEquiv

added theorem MvPolynomial.support_finSuccEquiv_nonempty