Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-24 05:52 ed07cac5

View on Github →

feat(data/mv_polynomial/rename): coeff_rename (#4203) Also, use the opportunity to use R as variable for the coefficient ring throughout the file.

Estimated changes

Modified src/data/mv_polynomial/rename.lean

added theorem mv_polynomial.coeff_rename_eq_zero

added theorem mv_polynomial.coeff_rename_map_domain

added theorem mv_polynomial.coeff_rename_ne_zero

modified theorem mv_polynomial.eval_rename_prodmk

modified theorem mv_polynomial.eval₂_cast_comp

modified theorem mv_polynomial.eval₂_rename_prodmk

modified theorem mv_polynomial.exists_fin_rename

modified theorem mv_polynomial.exists_finset_rename

modified theorem mv_polynomial.map_rename

modified def mv_polynomial.rename

modified theorem mv_polynomial.rename_C

modified theorem mv_polynomial.rename_X

modified theorem mv_polynomial.rename_eq

modified theorem mv_polynomial.rename_eval₂

modified theorem mv_polynomial.rename_id

modified theorem mv_polynomial.rename_injective

modified theorem mv_polynomial.rename_monomial

modified theorem mv_polynomial.rename_prodmk_eval₂

modified theorem mv_polynomial.rename_rename

modified theorem mv_polynomial.total_degree_rename_le