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} [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

• Polynomial.eraseLead f = Polynomial.erase (Polynomial.natDegree f) f

theorem Polynomial.eraseLead_support {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.support (Polynomial.eraseLead f) = Finset.erase (Polynomial.support f) (Polynomial.natDegree f)

theorem Polynomial.eraseLead_coeff {R : Type u_1} [Semiring R] {f : Polynomial R} (i : ℕ) : Polynomial.coeff (Polynomial.eraseLead f) i = if i = Polynomial.natDegree f then 0 else Polynomial.coeff f i

@[simp]

theorem Polynomial.eraseLead_coeff_natDegree {R : Type u_1} [Semiring R] {f : Polynomial R} : Polynomial.coeff (Polynomial.eraseLead f) (Polynomial.natDegree f) = 0

theorem Polynomial.eraseLead_coeff_of_ne {R : Type u_1} [Semiring R] {f : Polynomial R} (i : ℕ) (hi : i ≠ Polynomial.natDegree f) : Polynomial.coeff (Polynomial.eraseLead f) i = Polynomial.coeff f i

@[simp]

theorem Polynomial.eraseLead_zero {R : Type u_1} [Semiring R] : Polynomial.eraseLead 0 = 0

@[simp]

theorem Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.eraseLead f + ↑(Polynomial.monomial (Polynomial.natDegree f)) (Polynomial.leadingCoeff f) = f

@[simp]

theorem Polynomial.eraseLead_add_C_mul_X_pow {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.eraseLead f + ↑Polynomial.C (Polynomial.leadingCoeff f) * Polynomial.X ^ Polynomial.natDegree f = f

@[simp]

theorem Polynomial.self_sub_monomial_natDegree_leadingCoeff {R : Type u_2} [Ring R] (f : Polynomial R) : f - ↑(Polynomial.monomial (Polynomial.natDegree f)) (Polynomial.leadingCoeff f) = Polynomial.eraseLead f

@[simp]

theorem Polynomial.self_sub_C_mul_X_pow {R : Type u_2} [Ring R] (f : Polynomial R) : f - ↑Polynomial.C (Polynomial.leadingCoeff f) * Polynomial.X ^ Polynomial.natDegree f = Polynomial.eraseLead f

theorem Polynomial.eraseLead_ne_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (f0 : 2 ≤ Finset.card (Polynomial.support f)) : Polynomial.eraseLead f ≠ 0

theorem Polynomial.lt_natDegree_of_mem_eraseLead_support {R : Type u_1} [Semiring R] {f : Polynomial R} {a : ℕ} (h : a ∈ Polynomial.support (Polynomial.eraseLead f)) : a < Polynomial.natDegree f

theorem Polynomial.ne_natDegree_of_mem_eraseLead_support {R : Type u_1} [Semiring R] {f : Polynomial R} {a : ℕ} (h : a ∈ Polynomial.support (Polynomial.eraseLead f)) : a ≠ Polynomial.natDegree f

theorem Polynomial.natDegree_not_mem_eraseLead_support {R : Type u_1} [Semiring R] {f : Polynomial R} : ¬Polynomial.natDegree f ∈ Polynomial.support (Polynomial.eraseLead f)

theorem Polynomial.eraseLead_support_card_lt {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f ≠ 0) : Finset.card (Polynomial.support (Polynomial.eraseLead f)) < Finset.card (Polynomial.support f)

theorem Polynomial.eraseLead_card_support {R : Type u_1} [Semiring R] {f : Polynomial R} {c : ℕ} (fc : Finset.card (Polynomial.support f) = c) : Finset.card (Polynomial.support (Polynomial.eraseLead f)) = c - 1

theorem Polynomial.eraseLead_card_support' {R : Type u_1} [Semiring R] {f : Polynomial R} {c : ℕ} (fc : Finset.card (Polynomial.support f) = c + 1) : Finset.card (Polynomial.support (Polynomial.eraseLead f)) = c

@[simp]

theorem Polynomial.eraseLead_monomial {R : Type u_1} [Semiring R] (i : ℕ) (r : R) : Polynomial.eraseLead (↑(Polynomial.monomial i) r) = 0

@[simp]

theorem Polynomial.eraseLead_C {R : Type u_1} [Semiring R] (r : R) : Polynomial.eraseLead (↑Polynomial.C r) = 0

@[simp]

theorem Polynomial.eraseLead_X {R : Type u_1} [Semiring R] : Polynomial.eraseLead Polynomial.X = 0

@[simp]

theorem Polynomial.eraseLead_X_pow {R : Type u_1} [Semiring R] (n : ℕ) : Polynomial.eraseLead (Polynomial.X ^ n) = 0

@[simp]

theorem Polynomial.eraseLead_C_mul_X_pow {R : Type u_1} [Semiring R] (r : R) (n : ℕ) : Polynomial.eraseLead (↑Polynomial.C r * Polynomial.X ^ n) = 0

theorem Polynomial.eraseLead_add_of_natDegree_lt_left {R : Type u_1} [Semiring R] {p : Polynomial R} {q : Polynomial R} (pq : Polynomial.natDegree q < Polynomial.natDegree p) : Polynomial.eraseLead (p + q) = Polynomial.eraseLead p + q

theorem Polynomial.eraseLead_add_of_natDegree_lt_right {R : Type u_1} [Semiring R] {p : Polynomial R} {q : Polynomial R} (pq : Polynomial.natDegree p < Polynomial.natDegree q) : Polynomial.eraseLead (p + q) = p + Polynomial.eraseLead q

theorem Polynomial.eraseLead_degree_le {R : Type u_1} [Semiring R] {f : Polynomial R} : Polynomial.degree (Polynomial.eraseLead f) ≤ Polynomial.degree f

theorem Polynomial.eraseLead_natDegree_le_aux {R : Type u_1} [Semiring R] {f : Polynomial R} : Polynomial.natDegree (Polynomial.eraseLead f) ≤ Polynomial.natDegree f

theorem Polynomial.eraseLead_natDegree_lt {R : Type u_1} [Semiring R] {f : Polynomial R} (f0 : 2 ≤ Finset.card (Polynomial.support f)) : Polynomial.natDegree (Polynomial.eraseLead f) < Polynomial.natDegree f

theorem Polynomial.eraseLead_natDegree_lt_or_eraseLead_eq_zero {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.natDegree (Polynomial.eraseLead f) < Polynomial.natDegree f ∨ Polynomial.eraseLead f = 0

theorem Polynomial.eraseLead_natDegree_le {R : Type u_1} [Semiring R] (f : Polynomial R) : Polynomial.natDegree (Polynomial.eraseLead f) ≤ Polynomial.natDegree f - 1

theorem Polynomial.induction_with_natDegree_le {R : Type u_1} [Semiring R] (P : Polynomial R → Prop) (N : ℕ) (P_0 : P 0) (P_C_mul_pow : (n : ℕ) → (r : R) → r ≠ 0 → n ≤ N → P (↑Polynomial.C r * Polynomial.X ^ n)) (P_C_add : (f g : Polynomial R) → Polynomial.natDegree f < Polynomial.natDegree g → Polynomial.natDegree g ≤ N → P f → P g → P (f + g)) (f : Polynomial R) : Polynomial.natDegree f ≤ N → 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} [Semiring R] {S : Type u_2} {F : Type u_3} [Semiring 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}, Polynomial.natDegree f < k → ↑φ f = 0) (φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → Polynomial.natDegree (↑φ (↑(Polynomial.monomial n) c)) = fu n) : Polynomial.natDegree (↑φ p) = fu (Polynomial.natDegree p)

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

theorem Polynomial.map_natDegree_eq_natDegree {R : Type u_1} [Semiring R] {S : Type u_2} {F : Type u_3} [Semiring S] [AddMonoidHomClass F (Polynomial R) (Polynomial S)] {φ : F} (p : Polynomial R) (φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → Polynomial.natDegree (↑φ (↑(Polynomial.monomial n) c)) = n) : Polynomial.natDegree (↑φ p) = Polynomial.natDegree p

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) : 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} [Semiring R] {f : Polynomial R} {n : ℕ} : Finset.card (Polynomial.support 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} [Semiring R] {f : Polynomial R} : Finset.card (Polynomial.support f) = 1 ↔ ∃ k x hx, f = ↑Polynomial.C x * Polynomial.X ^ k

theorem Polynomial.card_support_eq_two {R : Type u_1} [Semiring R] {f : Polynomial R} : Finset.card (Polynomial.support f) = 2 ↔ ∃ 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} [Semiring R] {f : Polynomial R} : Finset.card (Polynomial.support f) = 3 ↔ ∃ 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