Documentation

Mathlib.Algebra.Polynomial.EraseLead

Erase the leading term of a univariate polynomial #

Definition #

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.

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

Equations
Instances For
    theorem Polynomial.eraseLead_support {R : Type u_1} [Semiring R] (f : Polynomial R) :
    f.eraseLead.support = f.support.erase f.natDegree
    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
    @[simp]
    theorem Polynomial.eraseLead_coeff_natDegree {R : Type u_1} [Semiring R] {f : Polynomial R} :
    f.eraseLead.coeff f.natDegree = 0
    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
    @[simp]
    theorem Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff {R : Type u_1} [Semiring R] (f : Polynomial R) :
    f.eraseLead + (Polynomial.monomial f.natDegree) f.leadingCoeff = f
    @[simp]
    theorem Polynomial.eraseLead_add_C_mul_X_pow {R : Type u_1} [Semiring R] (f : Polynomial R) :
    f.eraseLead + Polynomial.C f.leadingCoeff * Polynomial.X ^ f.natDegree = f
    @[simp]
    theorem Polynomial.self_sub_monomial_natDegree_leadingCoeff {R : Type u_2} [Ring R] (f : Polynomial R) :
    f - (Polynomial.monomial f.natDegree) f.leadingCoeff = f.eraseLead
    @[simp]
    theorem Polynomial.self_sub_C_mul_X_pow {R : Type u_2} [Ring R] (f : Polynomial R) :
    f - Polynomial.C f.leadingCoeff * Polynomial.X ^ f.natDegree = f.eraseLead
    theorem Polynomial.eraseLead_ne_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (f0 : 2 f.support.card) :
    f.eraseLead 0
    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
    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
    theorem Polynomial.natDegree_not_mem_eraseLead_support {R : Type u_1} [Semiring R] {f : Polynomial R} :
    f.natDegreef.eraseLead.support
    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
    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
    @[simp]
    theorem Polynomial.card_support_eraseLead {R : Type u_1} [Semiring R] {f : Polynomial R} :
    f.eraseLead.support.card = f.support.card - 1
    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
    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
    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
    @[simp]
    theorem Polynomial.eraseLead_monomial {R : Type u_1} [Semiring R] (i : ) (r : R) :
    ((Polynomial.monomial i) r).eraseLead = 0
    @[simp]
    theorem Polynomial.eraseLead_C {R : Type u_1} [Semiring R] (r : R) :
    (Polynomial.C r).eraseLead = 0
    @[simp]
    theorem Polynomial.eraseLead_X {R : Type u_1} [Semiring R] :
    Polynomial.X.eraseLead = 0
    @[simp]
    theorem Polynomial.eraseLead_X_pow {R : Type u_1} [Semiring R] (n : ) :
    (Polynomial.X ^ n).eraseLead = 0
    @[simp]
    theorem Polynomial.eraseLead_C_mul_X_pow {R : Type u_1} [Semiring R] (r : R) (n : ) :
    (Polynomial.C r * Polynomial.X ^ n).eraseLead = 0
    @[simp]
    theorem Polynomial.eraseLead_C_mul_X {R : Type u_1} [Semiring R] (r : R) :
    (Polynomial.C r * Polynomial.X).eraseLead = 0
    theorem Polynomial.eraseLead_add_of_degree_lt_left {R : Type u_1} [Semiring R] {p : Polynomial R} {q : Polynomial R} (pq : q.degree < p.degree) :
    (p + q).eraseLead = p.eraseLead + q
    theorem Polynomial.eraseLead_add_of_natDegree_lt_left {R : Type u_1} [Semiring R] {p : Polynomial R} {q : Polynomial R} (pq : q.natDegree < p.natDegree) :
    (p + q).eraseLead = p.eraseLead + q
    theorem Polynomial.eraseLead_add_of_degree_lt_right {R : Type u_1} [Semiring R] {p : Polynomial R} {q : Polynomial R} (pq : p.degree < q.degree) :
    (p + q).eraseLead = p + q.eraseLead
    theorem Polynomial.eraseLead_add_of_natDegree_lt_right {R : Type u_1} [Semiring R] {p : Polynomial R} {q : Polynomial R} (pq : p.natDegree < q.natDegree) :
    (p + q).eraseLead = p + q.eraseLead
    theorem Polynomial.eraseLead_degree_le {R : Type u_1} [Semiring R] {f : Polynomial R} :
    f.eraseLead.degree f.degree
    theorem Polynomial.degree_eraseLead_lt {R : Type u_1} [Semiring R] {f : Polynomial R} (hf : f 0) :
    f.eraseLead.degree < f.degree
    theorem Polynomial.eraseLead_natDegree_le_aux {R : Type u_1} [Semiring R] {f : Polynomial R} :
    f.eraseLead.natDegree f.natDegree
    theorem Polynomial.eraseLead_natDegree_lt {R : Type u_1} [Semiring R] {f : Polynomial R} (f0 : 2 f.support.card) :
    f.eraseLead.natDegree < f.natDegree
    theorem Polynomial.natDegree_pos_of_eraseLead_ne_zero {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.eraseLead 0) :
    0 < f.natDegree
    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
    theorem Polynomial.eraseLead_natDegree_le {R : Type u_1} [Semiring R] (f : Polynomial R) :
    f.eraseLead.natDegree f.natDegree - 1
    theorem Polynomial.natDegree_eraseLead {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.nextCoeff 0) :
    f.eraseLead.natDegree = f.natDegree - 1
    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
    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
    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
    theorem Polynomial.leadingCoeff_eraseLead_eq_nextCoeff {R : Type u_1} [Semiring R] {f : Polynomial R} (h : f.nextCoeff 0) :
    f.eraseLead.leadingCoeff = f.nextCoeff
    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
    theorem Polynomial.induction_with_natDegree_le {R : Type u_1} [Semiring R] (P : Polynomial RProp) (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 : Polynomial R), f.natDegree < g.natDegreeg.natDegree NP fP gP (f + g)) (f : Polynomial R) :
    f.natDegree 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_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 kfu n = 0) (fc : ∀ {n m : }, k nn < mfu n < fu m) (φ_k : ∀ {f : Polynomial R}, f.natDegree < kφ f = 0) (φ_mon_nat : ∀ (n : ) (c : R), c 0(φ ((Polynomial.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).
    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(φ ((Polynomial.monomial n) c)).natDegree = n - k) :
    (φ p).natDegree = p.natDegree - k
    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(φ ((Polynomial.monomial n) c)).natDegree = n) :
    (φ p).natDegree = p.natDegree
    theorem Polynomial.card_support_eq' {R : Type u_1} [Semiring R] {n : } (k : Fin n) (x : Fin nR) (hk : Function.Injective k) (hx : ∀ (i : Fin n), x i 0) :
    (∑ i : Fin n, Polynomial.C (x i) * Polynomial.X ^ k i).support.card = n
    theorem Polynomial.card_support_eq {R : Type u_1} [Semiring R] {f : Polynomial R} {n : } :
    f.support.card = n ∃ (k : Fin n) (x : Fin nR) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i 0), f = 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) (_ : x 0), f = Polynomial.C x * Polynomial.X ^ k
    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 = 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} :
    f.support.card = 3 ∃ (k : ) (m : ) (n : ) (_ : k < m) (_ : m < n) (x : R) (y : R) (z : R) (_ : x 0) (_ : y 0) (_ : z 0), f = Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n