Commit 2023-03-08 14:42 c7d26d40

View on Github →

feat: port Data.Polynomial.EraseLead (#2721)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/EraseLead.lean

added theorem Polynomial.card_support_eq'

added theorem Polynomial.card_support_eq

added theorem Polynomial.card_support_eq_one

added theorem Polynomial.card_support_eq_three

added theorem Polynomial.card_support_eq_two

added def Polynomial.eraseLead

added theorem Polynomial.eraseLead_C

added theorem Polynomial.eraseLead_C_mul_X_pow

added theorem Polynomial.eraseLead_X

added theorem Polynomial.eraseLead_X_pow

added theorem Polynomial.eraseLead_add_C_mul_X_pow

added theorem Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff

added theorem Polynomial.eraseLead_add_of_natDegree_lt_left

added theorem Polynomial.eraseLead_add_of_natDegree_lt_right

added theorem Polynomial.eraseLead_card_support'

added theorem Polynomial.eraseLead_card_support

added theorem Polynomial.eraseLead_coeff

added theorem Polynomial.eraseLead_coeff_natDegree

added theorem Polynomial.eraseLead_coeff_of_ne

added theorem Polynomial.eraseLead_degree_le

added theorem Polynomial.eraseLead_monomial

added theorem Polynomial.eraseLead_natDegree_le

added theorem Polynomial.eraseLead_natDegree_le_aux

added theorem Polynomial.eraseLead_natDegree_lt

added theorem Polynomial.eraseLead_natDegree_lt_or_eraseLead_eq_zero

added theorem Polynomial.eraseLead_ne_zero

added theorem Polynomial.eraseLead_support

added theorem Polynomial.eraseLead_support_card_lt

added theorem Polynomial.eraseLead_zero

added theorem Polynomial.induction_with_natDegree_le

added theorem Polynomial.lt_natDegree_of_mem_eraseLead_support

added theorem Polynomial.map_natDegree_eq_natDegree

added theorem Polynomial.map_natDegree_eq_sub

added theorem Polynomial.mono_map_natDegree_eq

added theorem Polynomial.natDegree_not_mem_eraseLead_support

added theorem Polynomial.ne_natDegree_of_mem_eraseLead_support

added theorem Polynomial.self_sub_C_mul_X_pow

added theorem Polynomial.self_sub_monomial_natDegree_leadingCoeff