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.

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]
theorem polynomial.erase_lead_add_C_mul_X_pow {R : Type u_1} [semiring R] (f : polynomial R) :
= f
@[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) :
@[simp]
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_degree_le {R : Type u_1} [semiring R] {f : polynomial R} :
theorem polynomial.erase_lead_nat_degree_le {R : Type u_1} [semiring R] {f : polynomial R} :
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 0n NP ((polynomial.C r) * ) (P_C_add : ∀ (f g : , g.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.

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 kfu n = 0) (fc : ∀ {n m : }, k nn < mfu 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) :