Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-11 21:06 3492206f

View on Github →

feat(data/mv_polynomial): misc lemmas on rename, map, and eval2 (#1127)

Estimated changes

Modified src/data/mv_polynomial.lean

added theorem mv_polynomial.coeff_X

added theorem mv_polynomial.eval₂_comp_right

added theorem mv_polynomial.map_eval₂

added theorem mv_polynomial.map_rename

added theorem mv_polynomial.rename_add

added theorem mv_polynomial.rename_mul

added theorem mv_polynomial.rename_one

added theorem mv_polynomial.rename_pow

added theorem mv_polynomial.rename_sub

added theorem mv_polynomial.rename_zero