mathlib documentation


Erase the leading term of a univariate polynomial


erase_lead serves as reduction step in an induction, shaving off one monomial from a polynomial. The definition is set up so that it does not mention subtraction in the definition, and thus works for polynomials over semirings as well as rings.

def polynomial.erase_lead {R : Type u_1} [semiring R] (f : polynomial R) :

erase_lead f for a polynomial f is the polynomial obtained by subtracting from f the leading term of f.

theorem polynomial.erase_lead_coeff {R : Type u_1} [semiring R] {f : polynomial R} (i : ) :
f.erase_lead.coeff i = ite (i = f.nat_degree) 0 (f.coeff i)


theorem polynomial.erase_lead_coeff_of_ne {R : Type u_1} [semiring R] {f : polynomial R} (i : ) (hi : i f.nat_degree) :

theorem polynomial.erase_lead_zero {R : Type u_1} [semiring R] :

theorem polynomial.erase_lead_ne_zero {R : Type u_1} [semiring R] {f : polynomial R} (f0 : 2 :

theorem polynomial.erase_lead_monomial {R : Type u_1} [semiring R] (i : ) (r : R) :

theorem polynomial.erase_lead_C {R : Type u_1} [semiring R] (r : R) :

theorem polynomial.erase_lead_X {R : Type u_1} [semiring R] :

theorem polynomial.erase_lead_X_pow {R : Type u_1} [semiring R] (n : ) :

theorem polynomial.erase_lead_C_mul_X_pow {R : Type u_1} [semiring R] (r : R) (n : ) :