Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-12 10:16 8fa91251

View on Github →

feat(data/polynomial/degree/erase_lead): definition and basic lemmas (#4527) erase_lead serves as the reduction step in an induction, breaking off one monomial from a polynomial. It is used in a later PR to prove that reverse is a multiplicative monoid map on polynomials.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.pred_card_le_card_erase

added theorem finset.subset_of_eq

Modified src/data/finsupp/basic.lean

added theorem finsupp.card_support_eq_one'

added theorem finsupp.card_support_eq_one

added theorem finsupp.card_support_eq_zero

added theorem finsupp.eq_single_iff

added theorem finsupp.erase_zero

added theorem finsupp.support_eq_singleton'

added theorem finsupp.support_eq_singleton

Modified src/data/polynomial/basic.lean

added theorem polynomial.X_pow_eq_monomial

deleted theorem polynomial.monomial_eq_X_pow

Modified src/data/polynomial/degree.lean

added theorem polynomial.C_mul_X_pow_eq_self

added theorem polynomial.monomial_nat_degree_leading_coeff_eq_self

Modified src/data/polynomial/degree/basic.lean

added theorem polynomial.leading_coeff_monomial'

added theorem polynomial.nat_degree_monomial

Created src/data/polynomial/erase_lead.lean

added def polynomial.erase_lead

added theorem polynomial.erase_lead_C

added theorem polynomial.erase_lead_C_mul_X_pow

added theorem polynomial.erase_lead_X

added theorem polynomial.erase_lead_X_pow

added theorem polynomial.erase_lead_add_C_mul_X_pow

added theorem polynomial.erase_lead_add_monomial_nat_degree_leading_coeff

added theorem polynomial.erase_lead_coeff

added theorem polynomial.erase_lead_coeff_nat_degree

added theorem polynomial.erase_lead_coeff_of_ne

added theorem polynomial.erase_lead_degree_le

added theorem polynomial.erase_lead_monomial

added theorem polynomial.erase_lead_nat_degree_le

added theorem polynomial.erase_lead_nat_degree_lt

added theorem polynomial.erase_lead_ne_zero

added theorem polynomial.erase_lead_support

added theorem polynomial.erase_lead_support_card_lt

added theorem polynomial.erase_lead_zero

added theorem polynomial.nat_degree_not_mem_erase_lead_support

added theorem polynomial.ne_nat_degree_of_mem_erase_lead_support

added theorem polynomial.self_sub_C_mul_X_pow

added theorem polynomial.self_sub_monomial_nat_degree_leading_coeff