Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-06 06:48 62963861

View on Github →

feat(data/mv_polynomial): fill in API for vars (#4018) mv_polynomial.vars was missing a lot of API. This doesn't cover everything, but it fleshes out the theory quite a bit. There's probably more coming eventually -- this is what we have now. Co-authored by: Johan Commelin johan@commelin.net

Estimated changes

Modified src/data/mv_polynomial.lean

added theorem mv_polynomial.aeval_eq_constant_coeff_of_vars

added theorem mv_polynomial.degrees_add_of_disjoint

added theorem mv_polynomial.degrees_map

added theorem mv_polynomial.degrees_map_of_injective

added theorem mv_polynomial.eval₂_hom_eq_constant_coeff_of_vars

added theorem mv_polynomial.le_degrees_add

added theorem mv_polynomial.mem_degrees

added theorem mv_polynomial.mem_vars

added theorem mv_polynomial.support_map_of_injective

added theorem mv_polynomial.support_map_subset

added theorem mv_polynomial.vars_add_of_disjoint

added theorem mv_polynomial.vars_add_subset

added theorem mv_polynomial.vars_eq_support_bind_support

added theorem mv_polynomial.vars_map

added theorem mv_polynomial.vars_map_of_injective

added theorem mv_polynomial.vars_monomial_single

added theorem mv_polynomial.vars_neg

added theorem mv_polynomial.vars_sub_of_disjoint

added theorem mv_polynomial.vars_sub_subset

added theorem mv_polynomial.vars_sum_of_disjoint

added theorem mv_polynomial.vars_sum_subset