# Erase the leading term of a univariate polynomial #

## Definition #

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

eraseLead 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.eraseLead {R : Type u_1} [] (f : ) :

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

Instances For
theorem Polynomial.eraseLead_support {R : Type u_1} [] (f : ) :
theorem Polynomial.eraseLead_coeff {R : Type u_1} [] {f : } (i : ) :
= if then 0 else
@[simp]
theorem Polynomial.eraseLead_coeff_natDegree {R : Type u_1} [] {f : } :
theorem Polynomial.eraseLead_coeff_of_ne {R : Type u_1} [] {f : } (i : ) (hi : ) :
@[simp]
theorem Polynomial.eraseLead_zero {R : Type u_1} [] :
@[simp]
+ Polynomial.C () * Polynomial.X ^ = f
@[simp]
theorem Polynomial.self_sub_C_mul_X_pow {R : Type u_2} [Ring R] (f : ) :
f - Polynomial.C () * Polynomial.X ^ =
theorem Polynomial.eraseLead_ne_zero {R : Type u_1} [] {f : } (f0 : ) :
theorem Polynomial.lt_natDegree_of_mem_eraseLead_support {R : Type u_1} [] {f : } {a : } (h : ) :
theorem Polynomial.ne_natDegree_of_mem_eraseLead_support {R : Type u_1} [] {f : } {a : } (h : ) :
theorem Polynomial.eraseLead_support_card_lt {R : Type u_1} [] {f : } (h : f 0) :
theorem Polynomial.eraseLead_card_support {R : Type u_1} [] {f : } {c : } (fc : ) :
theorem Polynomial.eraseLead_card_support' {R : Type u_1} [] {f : } {c : } (fc : = c + 1) :
@[simp]
theorem Polynomial.eraseLead_monomial {R : Type u_1} [] (i : ) (r : R) :
= 0
@[simp]
theorem Polynomial.eraseLead_C {R : Type u_1} [] (r : R) :
@[simp]
theorem Polynomial.eraseLead_X {R : Type u_1} [] :
@[simp]
theorem Polynomial.eraseLead_X_pow {R : Type u_1} [] (n : ) :
Polynomial.eraseLead (Polynomial.X ^ n) = 0
@[simp]
theorem Polynomial.eraseLead_C_mul_X_pow {R : Type u_1} [] (r : R) (n : ) :
Polynomial.eraseLead (Polynomial.C r * Polynomial.X ^ n) = 0
theorem Polynomial.eraseLead_add_of_natDegree_lt_left {R : Type u_1} [] {p : } {q : } (pq : ) :
theorem Polynomial.eraseLead_add_of_natDegree_lt_right {R : Type u_1} [] {p : } {q : } (pq : ) :
theorem Polynomial.eraseLead_degree_le {R : Type u_1} [] {f : } :
theorem Polynomial.eraseLead_natDegree_lt {R : Type u_1} [] {f : } (f0 : ) :
theorem Polynomial.eraseLead_natDegree_le {R : Type u_1} [] (f : ) :
theorem Polynomial.induction_with_natDegree_le {R : Type u_1} [] (P : ) (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 : ) → P fP gP (f + g)) (f : ) :
P 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_natDegree_eq {R : Type u_1} [] {S : Type u_2} {F : Type u_3} [] [AddMonoidHomClass F () ()] {φ : F} {p : } (k : ) (fu : ) (fu0 : ∀ {n : }, n kfu n = 0) (fc : ∀ {n m : }, k nn < mfu n < fu m) (φ_k : ∀ {f : }, φ f = 0) (φ_mon_nat : ∀ (n : ) (c : R), c 0Polynomial.natDegree (φ (↑() c)) = fu n) :
Polynomial.natDegree (φ p) = fu ()

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_natDegree_eq_sub {R : Type u_1} [] {S : Type u_2} {F : Type u_3} [] [AddMonoidHomClass F () ()] {φ : F} {p : } {k : } (φ_k : ∀ (f : ), φ f = 0) (φ_mon : ∀ (n : ) (c : R), c 0Polynomial.natDegree (φ (↑() c)) = n - k) :
theorem Polynomial.map_natDegree_eq_natDegree {R : Type u_1} [] {S : Type u_2} {F : Type u_3} [] [AddMonoidHomClass F () ()] {φ : F} (p : ) (φ_mon_nat : ∀ (n : ) (c : R), c 0Polynomial.natDegree (φ (↑() c)) = n) :
theorem Polynomial.card_support_eq' {R : Type u_1} [] {n : } (k : Fin n) (x : Fin nR) (hk : ) (hx : ∀ (i : Fin n), x i 0) :
Finset.card (Polynomial.support (Finset.sum Finset.univ fun i => Polynomial.C (x i) * Polynomial.X ^ k i)) = n
theorem Polynomial.card_support_eq {R : Type u_1} [] {f : } {n : } :
k x hk hx, f = Finset.sum Finset.univ fun i => Polynomial.C (x i) * Polynomial.X ^ k i
theorem Polynomial.card_support_eq_one {R : Type u_1} [] {f : } :
k x hx, f = Polynomial.C x * Polynomial.X ^ k
theorem Polynomial.card_support_eq_two {R : Type u_1} [] {f : } :
k m hkm x y hx hy, f = Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m
theorem Polynomial.card_support_eq_three {R : Type u_1} [] {f : } :
k m n hkm hmn x y z hx hy hz, f = Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n