Erase the leading term of a univariate polynomial #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Definition #
erase_lead f: the polynomialf - leading term of f
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.
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_support
{R : Type u_1}
[semiring R]
(f : polynomial R) :
f.erase_lead.support = f.support.erase f.nat_degree
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_nat_degree
{R : Type u_1}
[semiring R]
{f : polynomial R} :
f.erase_lead.coeff f.nat_degree = 0
theorem
polynomial.erase_lead_coeff_of_ne
{R : Type u_1}
[semiring R]
{f : polynomial R}
(i : ℕ)
(hi : i ≠ f.nat_degree) :
f.erase_lead.coeff i = f.coeff i
@[simp]
theorem
polynomial.erase_lead_add_monomial_nat_degree_leading_coeff
{R : Type u_1}
[semiring R]
(f : polynomial R) :
f.erase_lead + ⇑(polynomial.monomial f.nat_degree) f.leading_coeff = f
@[simp]
theorem
polynomial.erase_lead_add_C_mul_X_pow
{R : Type u_1}
[semiring R]
(f : polynomial R) :
f.erase_lead + ⇑polynomial.C f.leading_coeff * polynomial.X ^ f.nat_degree = f
@[simp]
theorem
polynomial.self_sub_monomial_nat_degree_leading_coeff
{R : Type u_1}
[ring R]
(f : polynomial R) :
f - ⇑(polynomial.monomial f.nat_degree) f.leading_coeff = f.erase_lead
@[simp]
theorem
polynomial.self_sub_C_mul_X_pow
{R : Type u_1}
[ring R]
(f : polynomial R) :
f - ⇑polynomial.C f.leading_coeff * polynomial.X ^ f.nat_degree = f.erase_lead
theorem
polynomial.erase_lead_ne_zero
{R : Type u_1}
[semiring R]
{f : polynomial R}
(f0 : 2 ≤ f.support.card) :
f.erase_lead ≠ 0
theorem
polynomial.lt_nat_degree_of_mem_erase_lead_support
{R : Type u_1}
[semiring R]
{f : polynomial R}
{a : ℕ}
(h : a ∈ f.erase_lead.support) :
a < f.nat_degree
theorem
polynomial.ne_nat_degree_of_mem_erase_lead_support
{R : Type u_1}
[semiring R]
{f : polynomial R}
{a : ℕ}
(h : a ∈ f.erase_lead.support) :
a ≠ f.nat_degree
theorem
polynomial.nat_degree_not_mem_erase_lead_support
{R : Type u_1}
[semiring R]
{f : polynomial R} :
f.nat_degree ∉ f.erase_lead.support
theorem
polynomial.erase_lead_support_card_lt
{R : Type u_1}
[semiring R]
{f : polynomial R}
(h : f ≠ 0) :
theorem
polynomial.erase_lead_card_support
{R : Type u_1}
[semiring R]
{f : polynomial R}
{c : ℕ}
(fc : f.support.card = c) :
f.erase_lead.support.card = c - 1
theorem
polynomial.erase_lead_card_support'
{R : Type u_1}
[semiring R]
{f : polynomial R}
{c : ℕ}
(fc : f.support.card = c + 1) :
f.erase_lead.support.card = c
@[simp]
theorem
polynomial.erase_lead_monomial
{R : Type u_1}
[semiring R]
(i : ℕ)
(r : R) :
(⇑(polynomial.monomial i) r).erase_lead = 0
@[simp]
theorem
polynomial.erase_lead_C
{R : Type u_1}
[semiring R]
(r : R) :
(⇑polynomial.C r).erase_lead = 0
@[simp]
@[simp]
theorem
polynomial.erase_lead_X_pow
{R : Type u_1}
[semiring R]
(n : ℕ) :
(polynomial.X ^ n).erase_lead = 0
@[simp]
theorem
polynomial.erase_lead_C_mul_X_pow
{R : Type u_1}
[semiring R]
(r : R)
(n : ℕ) :
(⇑polynomial.C r * polynomial.X ^ n).erase_lead = 0
theorem
polynomial.erase_lead_add_of_nat_degree_lt_left
{R : Type u_1}
[semiring R]
{p q : polynomial R}
(pq : q.nat_degree < p.nat_degree) :
(p + q).erase_lead = p.erase_lead + q
theorem
polynomial.erase_lead_add_of_nat_degree_lt_right
{R : Type u_1}
[semiring R]
{p q : polynomial R}
(pq : p.nat_degree < q.nat_degree) :
(p + q).erase_lead = p + q.erase_lead
theorem
polynomial.erase_lead_degree_le
{R : Type u_1}
[semiring R]
{f : polynomial R} :
f.erase_lead.degree ≤ f.degree
theorem
polynomial.erase_lead_nat_degree_lt
{R : Type u_1}
[semiring R]
{f : polynomial R}
(f0 : 2 ≤ f.support.card) :
theorem
polynomial.erase_lead_nat_degree_lt_or_erase_lead_eq_zero
{R : Type u_1}
[semiring R]
(f : polynomial R) :
f.erase_lead.nat_degree < f.nat_degree ∨ f.erase_lead = 0
theorem
polynomial.erase_lead_nat_degree_le
{R : Type u_1}
[semiring R]
(f : polynomial R) :
f.erase_lead.nat_degree ≤ f.nat_degree - 1
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 ≠ 0 → n ≤ N → P (⇑polynomial.C r * polynomial.X ^ n))
(P_C_add : ∀ (f g : polynomial R), f.nat_degree < g.nat_degree → g.nat_degree ≤ N → P f → P g → P (f + g))
(f : polynomial R) :
f.nat_degree ≤ 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_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 ≤ k → fu n = 0)
(fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu 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) :
(⇑φ p).nat_degree = fu p.nat_degree
Let φ : R[x] → S[x] be an additive map, k : ℕ a bound, and fu : ℕ → ℕ a
"sufficiently monotone" map. Assume also that
φmaps to0all monomials of degree less thank,φmaps each monomialminR[x]to a polynomialφ mof degreefu (deg m). Then,φmaps each polynomialpinR[x]to a polynomial of degreefu (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) :
(⇑φ p).nat_degree = p.nat_degree - 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) :
(⇑φ p).nat_degree = p.nat_degree
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.univ.sum (λ (i : fin n), ⇑polynomial.C (x i) * polynomial.X ^ k i)).support.card = n
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