# Erase the leading term of a univariate polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Definition #

• erase_lead f: the polynomial f - leading term of f

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.

noncomputable 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_support {R : Type u_1} [semiring R] (f : polynomial R) :
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_nat_degree {R : Type u_1} [semiring R] {f : polynomial R} :
= 0
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] :
@[simp]
@[simp]
theorem polynomial.self_sub_C_mul_X_pow {R : Type u_1} [ring R] (f : polynomial 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_support_card_lt {R : Type u_1} [semiring R] {f : polynomial R} (h : f 0) :
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) :
= 0
@[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.erase_lead_nat_degree_lt {R : Type u_1} [semiring R] {f : polynomial R} (f0 : 2 f.support.card) :
theorem polynomial.induction_with_nat_degree_le {R : Type u_1} [semiring R] (P : Prop) (N : ) (P_0 : P 0) (P_C_mul_pow : (n : ) (r : R), r 0 n N P * ) (P_C_add : (f g : , g.nat_degree N P f P g P (f + g)) (f : polynomial R) :

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.

theorem polynomial.mono_map_nat_degree_eq {R : Type u_1} [semiring R] {S : Type u_2} {F : Type u_3} [semiring S] [ (polynomial S)] {φ : F} {p : polynomial R} (k : ) (fu : ) (fu0 : {n : }, n k fu n = 0) (fc : {n m : }, k n n < m fu n < fu m) (φ_k : {f : , f.nat_degree < k φ f = 0) (φ_mon_nat : (n : ) (c : R), c 0 (φ ( c)).nat_degree = fu n) :

Let φ : R[x] → S[x] be an additive map, k : ℕ a bound, and fu : ℕ → ℕ a "sufficiently monotone" map. Assume also that

• φ maps to 0 all monomials of degree less than k,
• φ maps each monomial m in R[x] to a polynomial φ m of degree fu (deg m). Then, φ maps each polynomial p in R[x] to a polynomial of degree fu (deg p).
theorem polynomial.map_nat_degree_eq_sub {R : Type u_1} [semiring R] {S : Type u_2} {F : Type u_3} [semiring S] [ (polynomial S)] {φ : F} {p : polynomial R} {k : } (φ_k : (f : , f.nat_degree < k φ f = 0) (φ_mon : (n : ) (c : R), c 0 (φ ( c)).nat_degree = n - k) :
theorem polynomial.map_nat_degree_eq_nat_degree {R : Type u_1} [semiring R] {S : Type u_2} {F : Type u_3} [semiring S] [ (polynomial S)] {φ : F} (p : polynomial R) (φ_mon_nat : (n : ) (c : R), c 0 (φ ( c)).nat_degree = n) :
theorem polynomial.card_support_eq' {R : Type u_1} [semiring R] {n : } (k : fin n ) (x : fin n R) (hk : function.injective k) (hx : (i : fin n), x i 0) :
theorem polynomial.card_support_eq {R : Type u_1} [semiring R] {f : polynomial R} {n : } :
f.support.card = n (k : fin n ) (x : fin n R) (hk : (hx : (i : fin n), x i 0), f = finset.univ.sum (λ (i : fin n), polynomial.C (x i) * polynomial.X ^ k i)
theorem polynomial.card_support_eq_one {R : Type u_1} [semiring R] {f : polynomial R} :
f.support.card = 1 (k : ) (x : R) (hx : x 0), f =
theorem polynomial.card_support_eq_two {R : Type u_1} [semiring R] {f : polynomial R} :
f.support.card = 2 (k m : ) (hkm : k < m) (x y : R) (hx : x 0) (hy : y 0), f = +
theorem polynomial.card_support_eq_three {R : Type u_1} [semiring R] {f : polynomial R} :
f.support.card = 3 (k m n : ) (hkm : k < m) (hmn : m < n) (x y z : R) (hx : x 0) (hy : y 0) (hz : z 0), f = + +