# 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.

source
def Polynomial.eraseLead {R : Type u_1} [Semiring R] (f : Polynomial R) :
Polynomial R

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

Equations

- f.eraseLead = Polynomial.erase f.natDegree f

Instances For

source
theorem Polynomial.eraseLead_support {R : Type u_1} [Semiring R] (f : Polynomial R) :
f.eraseLead.support = f.support.erase f.natDegree
source
theorem Polynomial.eraseLead_coeff {R : Type u_1} [Semiring R] {f : Polynomial R} (i : ℕ) :
f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i
source
@[simp]
theorem Polynomial.eraseLead_coeff_natDegree {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.eraseLead.coeff f.natDegree = 0
source
theorem Polynomial.eraseLead_coeff_of_ne {R : Type u_1} [Semiring R] {f : Polynomial R} (i : ℕ) (hi : i ≠ f.natDegree) :
f.eraseLead.coeff i = f.coeff i
source
@[simp]
theorem Polynomial.eraseLead_zero {R : Type u_1} [Semiring R] :
eraseLead 0 = 0
source
@[simp]
theorem Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff {R : Type u_1} [Semiring R] (f : Polynomial R) :
f.eraseLead + (monomial f.natDegree) f.leadingCoeff = f
source
@[simp]
theorem Polynomial.eraseLead_add_C_mul_X_pow {R : Type u_1} [Semiring R] (f : Polynomial R) :
f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f
source
@[simp]
theorem Polynomial.self_sub_monomial_natDegree_leadingCoeff {R : Type u_2} [Ring R] (f : Polynomial R) :
f - (monomial f.natDegree) f.leadingCoeff = f.eraseLead
source
@[simp]
theorem Polynomial.self_sub_C_mul_X_pow {R : Type u_2} [Ring R] (f : Polynomial R) :
f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead
source
theorem Polynomial.eraseLead_ne_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (f0 : 2 ≤ f.support.card) :
f.eraseLead ≠ 0
source
theorem Polynomial.lt_natDegree_of_mem_eraseLead_support {R : Type u_1} [Semiring R] {f : Polynomial R} {a : ℕ} (h : a ∈ f.eraseLead.support) :
a < f.natDegree
source
theorem Polynomial.ne_natDegree_of_mem_eraseLead_support {R : Type u_1} [Semiring R] {f : Polynomial R} {a : ℕ} (h : a ∈ f.eraseLead.support) :
a ≠ f.natDegree
source
theorem Polynomial.natDegree_notMem_eraseLead_support {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.natDegree ∉ f.eraseLead.support
source
@[deprecated Polynomial.natDegree_notMem_eraseLead_support (since := "2025-05-23")]
theorem Polynomial.natDegree_not_mem_eraseLead_support {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.natDegree ∉ f.eraseLead.support

Alias of `Polynomial.natDegree_notMem_eraseLead_support`.

source
theorem Polynomial.eraseLead_support_card_lt {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f ≠ 0) :
f.eraseLead.support.card < f.support.card
source
theorem Polynomial.card_support_eraseLead_add_one {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f ≠ 0) :
f.eraseLead.support.card + 1 = f.support.card
source
@[simp]
theorem Polynomial.card_support_eraseLead {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.eraseLead.support.card = f.support.card - 1
source
theorem Polynomial.card_support_eraseLead' {R : Type u_1} [Semiring R] {f : Polynomial R} {c : ℕ} (fc : f.support.card = c + 1) :
f.eraseLead.support.card = c
source
theorem Polynomial.card_support_eq_one_of_eraseLead_eq_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (h₀ : f ≠ 0) (h₁ : f.eraseLead = 0) :
f.support.card = 1
source
theorem Polynomial.card_support_le_one_of_eraseLead_eq_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.eraseLead = 0) :
f.support.card ≤ 1
source
@[simp]
theorem Polynomial.eraseLead_monomial {R : Type u_1} [Semiring R] (i : ℕ) (r : R) :
((monomial i) r).eraseLead = 0
source
@[simp]
theorem Polynomial.eraseLead_C {R : Type u_1} [Semiring R] (r : R) :
(C r).eraseLead = 0
source
@[simp]
theorem Polynomial.eraseLead_X {R : Type u_1} [Semiring R] :
X.eraseLead = 0
source
@[simp]
theorem Polynomial.eraseLead_X_pow {R : Type u_1} [Semiring R] (n : ℕ) :
(X ^ n).eraseLead = 0
source
@[simp]
theorem Polynomial.eraseLead_C_mul_X_pow {R : Type u_1} [Semiring R] (r : R) (n : ℕ) :
(C r * X ^ n).eraseLead = 0
source
@[simp]
theorem Polynomial.eraseLead_C_mul_X {R : Type u_1} [Semiring R] (r : R) :
(C r * X).eraseLead = 0
source
theorem Polynomial.eraseLead_add_of_degree_lt_left {R : Type u_1} [Semiring R] {p q : Polynomial R} (pq : q.degree < p.degree) :
(p + q).eraseLead = p.eraseLead + q
source
theorem Polynomial.eraseLead_add_of_natDegree_lt_left {R : Type u_1} [Semiring R] {p q : Polynomial R} (pq : q.natDegree < p.natDegree) :
(p + q).eraseLead = p.eraseLead + q
source
theorem Polynomial.eraseLead_add_of_degree_lt_right {R : Type u_1} [Semiring R] {p q : Polynomial R} (pq : p.degree < q.degree) :
(p + q).eraseLead = p + q.eraseLead
source
theorem Polynomial.eraseLead_add_of_natDegree_lt_right {R : Type u_1} [Semiring R] {p q : Polynomial R} (pq : p.natDegree < q.natDegree) :
(p + q).eraseLead = p + q.eraseLead
source
theorem Polynomial.eraseLead_degree_le {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.eraseLead.degree ≤ f.degree
source
theorem Polynomial.degree_eraseLead_lt {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f ≠ 0) :
f.eraseLead.degree < f.degree
source
theorem Polynomial.eraseLead_natDegree_le_aux {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.eraseLead.natDegree ≤ f.natDegree
source
theorem Polynomial.eraseLead_natDegree_lt {R : Type u_1} [Semiring R] {f : Polynomial R} (f0 : 2 ≤ f.support.card) :
f.eraseLead.natDegree < f.natDegree
source
theorem Polynomial.natDegree_pos_of_eraseLead_ne_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.eraseLead ≠ 0) :
0 < f.natDegree
source
theorem Polynomial.eraseLead_natDegree_lt_or_eraseLead_eq_zero {R : Type u_1} [Semiring R] (f : Polynomial R) :
f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
source
theorem Polynomial.eraseLead_natDegree_le {R : Type u_1} [Semiring R] (f : Polynomial R) :
f.eraseLead.natDegree ≤ f.natDegree - 1
source
theorem Polynomial.natDegree_eraseLead {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.nextCoeff ≠ 0) :
f.eraseLead.natDegree = f.natDegree - 1
source
theorem Polynomial.natDegree_eraseLead_add_one {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.nextCoeff ≠ 0) :
f.eraseLead.natDegree + 1 = f.natDegree
source
theorem Polynomial.natDegree_eraseLead_le_of_nextCoeff_eq_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.nextCoeff = 0) :
f.eraseLead.natDegree ≤ f.natDegree - 2
source
theorem Polynomial.two_le_natDegree_of_nextCoeff_eraseLead {R : Type u_1} [Semiring R] {f : Polynomial R} (hlead : f.eraseLead ≠ 0) (hnext : f.nextCoeff = 0) :
2 ≤ f.natDegree
source
theorem Polynomial.leadingCoeff_eraseLead_eq_nextCoeff {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.nextCoeff ≠ 0) :
f.eraseLead.leadingCoeff = f.nextCoeff
source
theorem Polynomial.nextCoeff_eq_zero_of_eraseLead_eq_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.eraseLead = 0) :
f.nextCoeff = 0
source
theorem Polynomial.eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero {R : Type u_2} [Ring R] [NoZeroDivisors R] [Nontrivial R] {x : R} {P : Polynomial R} (hx : x ≠ 0) (h : P.nextCoeff = 0) :
((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

If we erase the leading coefficient of a `Polynomial.coeffList` like [+,0,...], and then multiply by a linear term, it's equivalent to erasing the first two coefficients of the product.

source
theorem Polynomial.induction_with_natDegree_le {R : Type u_1} [Semiring R] (motive : Polynomial R → Prop) (N : ℕ) (zero : motive 0) (C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)) (add : ∀ (f g : Polynomial R), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)) (f : Polynomial R) (df : f.natDegree ≤ N) :
motive 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 `natDegree` 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 `natDegree` of the polynomial itself and not on the specific `natDegree` of each term.

source
theorem Polynomial.mono_map_natDegree_eq {R : Type u_1} [Semiring R] {S : Type u_2} {F : Type u_3} [Semiring S] [FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (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 : Polynomial R}, f.natDegree < k → φ f = 0) (φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n) :
(φ p).natDegree = fu p.natDegree

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)`.

source
theorem Polynomial.map_natDegree_eq_sub {R : Type u_1} [Semiring R] {S : Type u_2} {F : Type u_3} [Semiring S] [FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F} {p : Polynomial R} {k : ℕ} (φ_k : ∀ (f : Polynomial R), f.natDegree < k → φ f = 0) (φ_mon : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n - k) :
(φ p).natDegree = p.natDegree - k
source
theorem Polynomial.map_natDegree_eq_natDegree {R : Type u_1} [Semiring R] {S : Type u_2} {F : Type u_3} [Semiring S] [FunLike F (Polynomial R) (Polynomial S)] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F} (p : Polynomial R) (φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = n) :
(φ p).natDegree = p.natDegree
source
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) :
(∑ i : Fin n, C (x i) * X ^ k i).support.card = n
source
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) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i : Fin n, C (x i) * X ^ k i
source
theorem Polynomial.card_support_eq_one {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.support.card = 1 ↔ ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = C x * X ^ k
source
theorem Polynomial.card_support_eq_two {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.support.card = 2 ↔ ∃ (k : ℕ) (m : ℕ) (_ : k < m) (x : R) (y : R) (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m
source
theorem Polynomial.card_support_eq_three {R : Type u_1} [Semiring R] {f : Polynomial R} :
f.support.card = 3 ↔ ∃ (k : ℕ) (m : ℕ) (n : ℕ) (_ : k < m) (_ : m < n) (x : R) (y : R) (z : R) (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n