Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-01 19:35 a2c291de

View on Github →

feat(data/mv_polynomial): miscellaneous lemmas on eval, rename, etc (#1134)

Estimated changes

Modified src/data/mv_polynomial.lean

added theorem mv_polynomial.C_eq_coe_nat

added theorem mv_polynomial.C_pow

modified theorem mv_polynomial.coeff_X

added theorem mv_polynomial.eval_rename_prodmk

added theorem mv_polynomial.eval₂_assoc

added theorem mv_polynomial.eval₂_congr

modified theorem mv_polynomial.eval₂_eta

modified theorem mv_polynomial.eval₂_mul

modified theorem mv_polynomial.eval₂_pow

added theorem mv_polynomial.eval₂_prod

added theorem mv_polynomial.eval₂_rename

added theorem mv_polynomial.eval₂_rename_prodmk

added theorem mv_polynomial.eval₂_sum

added theorem mv_polynomial.ext_iff

added theorem mv_polynomial.map_injective

added theorem mv_polynomial.map_pow

added theorem mv_polynomial.rename_eval₂

added theorem mv_polynomial.rename_prodmk_eval₂