Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-05 22:48 599df281

View on Github →

feat(linear_algebra/mv_polynomial): composition lemmas

Estimated changes

Modified linear_algebra/multivariate_polynomial.lean

modified def mv_polynomial.eval

modified theorem mv_polynomial.eval_C

modified theorem mv_polynomial.eval_X

modified theorem mv_polynomial.eval_add

added theorem mv_polynomial.eval_assoc

modified theorem mv_polynomial.eval_mul

modified theorem mv_polynomial.eval_zero

added def mv_polynomial.eval₂

added theorem mv_polynomial.eval₂_C

added theorem mv_polynomial.eval₂_X

added theorem mv_polynomial.eval₂_add

added theorem mv_polynomial.eval₂_comp_left

added theorem mv_polynomial.eval₂_eq_eval_map

added theorem mv_polynomial.eval₂_eta

added theorem mv_polynomial.eval₂_monomial

added theorem mv_polynomial.eval₂_mul

added theorem mv_polynomial.eval₂_mul_monomial

added theorem mv_polynomial.eval₂_one

added theorem mv_polynomial.eval₂_zero

modified def mv_polynomial.map

modified theorem mv_polynomial.map_C

modified theorem mv_polynomial.map_X

added theorem mv_polynomial.map_id

added theorem mv_polynomial.map_map

modified theorem mv_polynomial.map_one

deleted def mv_polynomial.map₂

deleted theorem mv_polynomial.map₂_C

deleted theorem mv_polynomial.map₂_X

deleted theorem mv_polynomial.map₂_add

deleted theorem mv_polynomial.map₂_monomial

deleted theorem mv_polynomial.map₂_mul

deleted theorem mv_polynomial.map₂_mul_monomial

deleted theorem mv_polynomial.map₂_one

deleted theorem mv_polynomial.map₂_zero