Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-05 09:21 78fd58dd

View on Github →

feat(linear_algebra/multivariate_polynomial): add degrees

Estimated changes

Modified src/linear_algebra/multivariate_polynomial.lean

modified def mv_polynomial.degree_of

added def mv_polynomial.degrees

added theorem mv_polynomial.degrees_C

added theorem mv_polynomial.degrees_X

added theorem mv_polynomial.degrees_add

added theorem mv_polynomial.degrees_monomial

added theorem mv_polynomial.degrees_monomial_eq

added theorem mv_polynomial.degrees_mul

added theorem mv_polynomial.degrees_neg

added theorem mv_polynomial.degrees_one

added theorem mv_polynomial.degrees_pow

added theorem mv_polynomial.degrees_prod

added theorem mv_polynomial.degrees_sub

added theorem mv_polynomial.degrees_sum

added theorem mv_polynomial.degrees_zero

modified def mv_polynomial.vars