Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-07 05:51 235129a8

View on Github →

feat(linear_algebra/multivariate_polynomial): Add _sub and _neg lemmas, and make them simp. (#238)

Estimated changes

modified theorem mv_polynomial.C_add
modified theorem mv_polynomial.C_mul
added theorem mv_polynomial.C_neg
added theorem mv_polynomial.C_sub
modified theorem mv_polynomial.eval_add
modified theorem mv_polynomial.eval_monomial
modified theorem mv_polynomial.eval_mul
added theorem mv_polynomial.eval_neg
added theorem mv_polynomial.eval_sub
modified theorem mv_polynomial.eval₂_add
added theorem mv_polynomial.map_neg
added theorem mv_polynomial.map_sub