Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-04 19:53 2d0eb8cc

View on Github →

feat(linear_algebra/mv_polynomial): map function, map2

Estimated changes

Modified data/finsupp.lean

added theorem finsupp.map_range_single

Modified linear_algebra/multivariate_polynomial.lean

added theorem mv_polynomial.C_add

added theorem mv_polynomial.C_mul

modified def mv_polynomial.eval

modified theorem mv_polynomial.eval_C

modified theorem mv_polynomial.eval_X

modified theorem mv_polynomial.eval_add

modified theorem mv_polynomial.eval_mul

deleted theorem mv_polynomial.eval_mul_monomial

modified theorem mv_polynomial.eval_zero

added def mv_polynomial.map

added theorem mv_polynomial.map_C

added theorem mv_polynomial.map_X

added theorem mv_polynomial.map_add

added theorem mv_polynomial.map_monomial

added theorem mv_polynomial.map_mul

added theorem mv_polynomial.map_one

added def mv_polynomial.map₂

added theorem mv_polynomial.map₂_C

added theorem mv_polynomial.map₂_X

added theorem mv_polynomial.map₂_add

added theorem mv_polynomial.map₂_monomial

added theorem mv_polynomial.map₂_mul

added theorem mv_polynomial.map₂_mul_monomial

added theorem mv_polynomial.map₂_one

added theorem mv_polynomial.map₂_zero