Commit 2023-03-18 07:59 45b747db

View on Github →

feat: port Data.MvPolynomial.Variables (#2961)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Variables.lean

added theorem MvPolynomial.aeval_eq_constantCoeff_of_vars

added theorem MvPolynomial.coeff_eq_zero_of_totalDegree_lt

added def MvPolynomial.degreeOf

added theorem MvPolynomial.degreeOf_C

added theorem MvPolynomial.degreeOf_X

added theorem MvPolynomial.degreeOf_add_le

added theorem MvPolynomial.degreeOf_eq_sup

added theorem MvPolynomial.degreeOf_lt_iff

added theorem MvPolynomial.degreeOf_mul_X_eq

added theorem MvPolynomial.degreeOf_mul_X_ne

added theorem MvPolynomial.degreeOf_mul_le

added theorem MvPolynomial.degreeOf_rename_of_injective

added theorem MvPolynomial.degreeOf_zero

added def MvPolynomial.degrees

added theorem MvPolynomial.degrees_C

added theorem MvPolynomial.degrees_X'

added theorem MvPolynomial.degrees_X

added theorem MvPolynomial.degrees_add

added theorem MvPolynomial.degrees_add_of_disjoint

added theorem MvPolynomial.degrees_map

added theorem MvPolynomial.degrees_map_of_injective

added theorem MvPolynomial.degrees_monomial

added theorem MvPolynomial.degrees_monomial_eq

added theorem MvPolynomial.degrees_mul

added theorem MvPolynomial.degrees_one

added theorem MvPolynomial.degrees_pow

added theorem MvPolynomial.degrees_prod

added theorem MvPolynomial.degrees_rename

added theorem MvPolynomial.degrees_rename_of_injective

added theorem MvPolynomial.degrees_sum

added theorem MvPolynomial.degrees_zero

added theorem MvPolynomial.eval₂Hom_congr'

added theorem MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars

added theorem MvPolynomial.exists_degree_lt

added theorem MvPolynomial.exists_rename_eq_of_vars_subset_range

added theorem MvPolynomial.hom_congr_vars

added theorem MvPolynomial.le_degrees_add

added theorem MvPolynomial.le_totalDegree

added theorem MvPolynomial.mem_degrees

added theorem MvPolynomial.mem_support_not_mem_vars_zero

added theorem MvPolynomial.mem_vars

added theorem MvPolynomial.mem_vars_rename

added theorem MvPolynomial.monomial_le_degreeOf

added def MvPolynomial.totalDegree

added theorem MvPolynomial.totalDegree_C

added theorem MvPolynomial.totalDegree_X

added theorem MvPolynomial.totalDegree_X_pow

added theorem MvPolynomial.totalDegree_add

added theorem MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt

added theorem MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt

added theorem MvPolynomial.totalDegree_eq

added theorem MvPolynomial.totalDegree_finset_prod

added theorem MvPolynomial.totalDegree_finset_sum

added theorem MvPolynomial.totalDegree_le_degrees_card

added theorem MvPolynomial.totalDegree_list_prod

added theorem MvPolynomial.totalDegree_monomial

added theorem MvPolynomial.totalDegree_mul

added theorem MvPolynomial.totalDegree_multiset_prod

added theorem MvPolynomial.totalDegree_one

added theorem MvPolynomial.totalDegree_pow

added theorem MvPolynomial.totalDegree_rename_le

added theorem MvPolynomial.totalDegree_smul_le

added theorem MvPolynomial.totalDegree_zero

added def MvPolynomial.vars

added theorem MvPolynomial.vars_0

added theorem MvPolynomial.vars_C

added theorem MvPolynomial.vars_C_mul

added theorem MvPolynomial.vars_X

added theorem MvPolynomial.vars_add_of_disjoint

added theorem MvPolynomial.vars_add_subset

added theorem MvPolynomial.vars_eq_support_bunionᵢ_support

added theorem MvPolynomial.vars_map

added theorem MvPolynomial.vars_map_of_injective

added theorem MvPolynomial.vars_monomial

added theorem MvPolynomial.vars_monomial_single

added theorem MvPolynomial.vars_mul

added theorem MvPolynomial.vars_one

added theorem MvPolynomial.vars_pow

added theorem MvPolynomial.vars_prod

added theorem MvPolynomial.vars_rename

added theorem MvPolynomial.vars_sum_of_disjoint

added theorem MvPolynomial.vars_sum_subset