Commit 2023-03-08 18:19 13b68bd9

View on Github →

feat: port Data.Polynomial.Degree.Lemmas (#2723)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Degree/Lemmas.lean

added theorem Polynomial.coe_lt_degree

added theorem Polynomial.coeff_add_eq_left_of_lt

added theorem Polynomial.coeff_add_eq_right_of_lt

added theorem Polynomial.coeff_mul_of_natDegree_le

added theorem Polynomial.coeff_pow_of_natDegree_le

added theorem Polynomial.coeff_sub_eq_left_of_lt

added theorem Polynomial.coeff_sub_eq_neg_right_of_lt

added theorem Polynomial.degree_C_mul

added theorem Polynomial.degree_mul_C

added theorem Polynomial.degree_pos_of_eval₂_root

added theorem Polynomial.degree_pos_of_root

added theorem Polynomial.degree_sum_eq_of_disjoint

added theorem Polynomial.eq_natDegree_of_le_mem_support

added theorem Polynomial.leadingCoeff_comp

added theorem Polynomial.natDegree_C_mul

added theorem Polynomial.natDegree_C_mul_eq_of_mul_eq_one

added theorem Polynomial.natDegree_C_mul_le

added theorem Polynomial.natDegree_add_coeff_mul

added theorem Polynomial.natDegree_add_le_iff_left

added theorem Polynomial.natDegree_add_le_iff_right

added theorem Polynomial.natDegree_bit0

added theorem Polynomial.natDegree_bit1

added theorem Polynomial.natDegree_c_mul_eq_of_mul_ne_zero

added theorem Polynomial.natDegree_comp

added theorem Polynomial.natDegree_comp_le

added theorem Polynomial.natDegree_le_iff_coeff_eq_zero

added theorem Polynomial.natDegree_lt_coeff_mul

added theorem Polynomial.natDegree_mul_C

added theorem Polynomial.natDegree_mul_C_eq_of_mul_eq_one

added theorem Polynomial.natDegree_mul_C_le

added theorem Polynomial.natDegree_mul_c_eq_of_mul_ne_zero

added theorem Polynomial.natDegree_pos_of_eval₂_root

added theorem Polynomial.natDegree_sub

added theorem Polynomial.natDegree_sub_le_iff_left

added theorem Polynomial.natDegree_sub_le_iff_right

added theorem Polynomial.natDegree_sum_eq_of_disjoint