Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-13 13:09 a2d61482

View on Github →

feat(algebra/linear_algebra): add multivariate polynomials

Estimated changes

Created algebra/linear_algebra/multivariate_polynomial.lean

added theorem finset.bind_singleton2

added theorem finset.le_sup

added def finset.sup

added theorem finset.sup_empty

added theorem finset.sup_insert

added theorem finset.sup_le

added theorem finset.sup_mono

added theorem finset.sup_mono_fun

added theorem finset.sup_singleton

added theorem finset.sup_union

added theorem finsupp.single_induction_on

added def mv_polynomial.C

added theorem mv_polynomial.C_0

added theorem mv_polynomial.C_1

added theorem mv_polynomial.C_mul_monomial

added def mv_polynomial.X

added theorem mv_polynomial.X_pow_eq_single

added def mv_polynomial.degree_of

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_monomial

added theorem mv_polynomial.eval_mul

added theorem mv_polynomial.eval_mul_monomial

added theorem mv_polynomial.eval_zero

added theorem mv_polynomial.induction_on

added def mv_polynomial.monomial

added theorem mv_polynomial.monomial_add_single

added theorem mv_polynomial.monomial_eq

added theorem mv_polynomial.monomial_single_add

added def mv_polynomial.total_degree

added def mv_polynomial.vars

added theorem mv_polynomial.vars_0

added theorem mv_polynomial.vars_C

added theorem mv_polynomial.vars_X

added theorem mv_polynomial.vars_monomial

added def mv_polynomial