mathlib documentation

data.polynomial.erase_lead

Erase the leading term of a univariate polynomial

Definition

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.

Equations
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)

@[simp]

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

@[simp]
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 f.support.card) :

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

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

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

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

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