Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-01 20:38 38b80546

View on Github →

feat(data/mv_polynomial): add coeff for mv_polynomial (#1101)

Estimated changes

Modified src/data/finsupp.lean

added theorem finsupp.nat_sub_apply

Modified src/data/mv_polynomial.lean

added def mv_polynomial.coeff

added theorem mv_polynomial.coeff_C

added theorem mv_polynomial.coeff_C_mul

added theorem mv_polynomial.coeff_add

added theorem mv_polynomial.coeff_map

added theorem mv_polynomial.coeff_monomial

added theorem mv_polynomial.coeff_mul_X'

added theorem mv_polynomial.coeff_mul_X

added theorem mv_polynomial.coeff_sub

added theorem mv_polynomial.coeff_sum

added theorem mv_polynomial.coeff_zero

added theorem mv_polynomial.coeff_zero_X

added theorem mv_polynomial.ext

added theorem mv_polynomial.monic_monomial_eq

added def mv_polynomial.tmp.coe