Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-25 12:54 c7d818cd

View on Github →

feat(data/mv_polynomial/variables): vars_bind₁ and friends (#4204) From the Witt vector project Co-Authored-By: Rob Y. Lewis rob.y.lewis@gmail.com

Estimated changes

Modified src/data/mv_polynomial/rename.lean

deleted theorem mv_polynomial.total_degree_rename_le

Modified src/data/mv_polynomial/variables.lean

modified theorem mv_polynomial.aeval_eq_constant_coeff_of_vars

added theorem mv_polynomial.degrees_rename

added theorem mv_polynomial.eval₂_hom_congr'

modified theorem mv_polynomial.eval₂_hom_eq_constant_coeff_of_vars

added theorem mv_polynomial.total_degree_rename_le

modified theorem mv_polynomial.vars_C

added theorem mv_polynomial.vars_bind₁

modified theorem mv_polynomial.vars_monomial

added theorem mv_polynomial.vars_rename