Erase the leading term of a univariate polynomial #
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 : R[X]) :
f.erase_lead.support = f.support.erase f.nat_degree
theorem
polynomial.erase_lead_coeff
{R : Type u_1}
[semiring R]
{f : R[X]}
(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 : R[X]} :
f.erase_lead.coeff f.nat_degree = 0
theorem
polynomial.erase_lead_coeff_of_ne
{R : Type u_1}
[semiring R]
{f : R[X]}
(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 : R[X]) :
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 : R[X]) :
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 : R[X]) :
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 : R[X]) :
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 : R[X]}
(f0 : 2 ≤ f.support.card) :
f.erase_lead ≠ 0
@[simp]
theorem
polynomial.nat_degree_not_mem_erase_lead_support
{R : Type u_1}
[semiring R]
{f : R[X]} :
f.nat_degree ∉ f.erase_lead.support
theorem
polynomial.ne_nat_degree_of_mem_erase_lead_support
{R : Type u_1}
[semiring R]
{f : R[X]}
{a : ℕ}
(h : a ∈ f.erase_lead.support) :
a ≠ f.nat_degree
@[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 : R[X]}
(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 : R[X]}
(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 : R[X]} :
f.erase_lead.degree ≤ f.degree
theorem
polynomial.erase_lead_nat_degree_lt_or_erase_lead_eq_zero
{R : Type u_1}
[semiring R]
(f : R[X]) :
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 : R[X]) :
f.erase_lead.nat_degree ≤ f.nat_degree - 1
theorem
polynomial.induction_with_nat_degree_le
{R : Type u_1}
[semiring R]
(P : R[X] → 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 : R[X]), f.nat_degree < g.nat_degree → g.nat_degree ≤ N → P f → P g → P (f + g))
(f : R[X]) :
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 R[X] S[X]]
{φ : F}
{p : R[X]}
(k : ℕ)
(fu : ℕ → ℕ)
(fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0)
(fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m)
(φ_k : ∀ {f : R[X]}, 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 R[X] S[X]]
{φ : F}
{p : R[X]}
{k : ℕ}
(φ_k : ∀ (f : R[X]), 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 R[X] S[X]]
{φ : F}
(p : R[X])
(φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (⇑φ (⇑(polynomial.monomial n) c)).nat_degree = n) :
(⇑φ p).nat_degree = p.nat_degree