Commit 2023-03-15 10:38 ee6a3f91

View on Github →

feat: port Data.MvPolynomial.Rename (#2886)

depends on: #2861

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Rename.lean

added theorem MvPolynomial.aeval_rename

added theorem MvPolynomial.coeff_rename_eq_zero

added theorem MvPolynomial.coeff_rename_mapDomain

added theorem MvPolynomial.coeff_rename_ne_zero

added theorem MvPolynomial.constantCoeff_rename

added theorem MvPolynomial.eval_rename_prod_mk

added theorem MvPolynomial.eval₂Hom_rename

added theorem MvPolynomial.eval₂_cast_comp

added theorem MvPolynomial.eval₂_rename

added theorem MvPolynomial.eval₂_rename_prod_mk

added theorem MvPolynomial.exists_fin_rename

added theorem MvPolynomial.exists_finset_rename

added theorem MvPolynomial.exists_finset_rename₂

added def MvPolynomial.killCompl

added theorem MvPolynomial.killCompl_comp_rename

added theorem MvPolynomial.killCompl_rename_app

added theorem MvPolynomial.map_rename

added def MvPolynomial.rename

added def MvPolynomial.renameEquiv

added theorem MvPolynomial.renameEquiv_refl

added theorem MvPolynomial.renameEquiv_symm

added theorem MvPolynomial.renameEquiv_trans

added theorem MvPolynomial.rename_C

added theorem MvPolynomial.rename_X

added theorem MvPolynomial.rename_eq

added theorem MvPolynomial.rename_eval₂

added theorem MvPolynomial.rename_id

added theorem MvPolynomial.rename_injective

added theorem MvPolynomial.rename_monomial

added theorem MvPolynomial.rename_prodmk_eval₂

added theorem MvPolynomial.rename_rename

added theorem MvPolynomial.support_rename_of_injective