mathlib documentation

data.polynomial.erase_lead

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_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_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] :
theorem polynomial.erase_lead_ne_zero {R : Type u_1} [semiring R] {f : polynomial R} (f0 : 2 f.support.card) :
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) :
@[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.induction_with_nat_degree_le {R : Type u_1} [semiring R] (P : polynomial R → Prop) (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.nat_degree < g.nat_degreeg.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] [add_monoid_hom_class 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.nat_degree < kφ f = 0) (φ_mon_nat : ∀ (n : ) (c : R), c 0(φ ((polynomial.monomial n) 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] [add_monoid_hom_class F (polynomial R) (polynomial S)] {φ : F} {p : polynomial R} {k : } (φ_k : ∀ (f : polynomial R), f.nat_degree < kφ f = 0) (φ_mon : ∀ (n : ) (c : R), c 0(φ ((polynomial.monomial n) 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] [add_monoid_hom_class F (polynomial R) (polynomial S)] {φ : F} (p : polynomial R) (φ_mon_nat : ∀ (n : ) (c : R), c 0(φ ((polynomial.monomial n) c)).nat_degree = n) :
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) :
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) (hk : strict_mono k) (hx : ∀ (i : fin n), x i 0), f = finset.univ.sum (λ (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) (hx : 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 : ) (hkm : k < m) (x y : R) (hx : x 0) (hy : 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 : ) (hkm : k < m) (hmn : m < n) (x y z : R) (hx : x 0) (hy : y 0) (hz : z 0), f = polynomial.C x * polynomial.X ^ k + polynomial.C y * polynomial.X ^ m + polynomial.C z * polynomial.X ^ n