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) :
theorem polynomial.erase_lead_card_support {R : Type u_1} [semiring R] {f : polynomial R} {c : } (fc : f.support.card = c) :
theorem polynomial.erase_lead_card_support' {R : Type u_1} [semiring R] {f : polynomial R} {c : } (fc : f.support.card = c + 1) :
@[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 : ) :
theorem polynomial.induction_with_nat_degree_le {R : Type u_1} [semiring R] {P : polynomial R → Prop} (N : ) (P_0 : P 0) (P_C_mul_pow : ∀ (n : ) (r : R), r 0n NP ((polynomial.C r) * polynomial.X ^ n)) (P_C_add : ∀ (f g : polynomial R), f.nat_degree Ng.nat_degree NP fP gP (f + g)) (f : polynomial R) :
f.nat_degree NP f

An induction lemma for polynomials. It takes a natural number N as a parameter, that is required to be at least as big as the nat_degree of the polynomial. This is useful to prove results where you want to change each term in a polynomial to something else depending on the nat_degree of the polynomial itself and not on the specific nat_degree of each term.