Cancel the leading terms of two polynomials

Definition

• cancelLeads p q: the polynomial formed by multiplying p and q by monomials so that they have the same leading term, and then subtracting.

Main Results

The degree of cancelLeads is less than that of the larger of the two polynomials being cancelled. Thus it is useful for induction or minimal-degree arguments.

noncomputable def Polynomial.cancelLeads {R : Type u_1} [Ring R] (p q : Polynomial R) : Polynomial R

cancelLeads p q is formed by multiplying p and q by monomials so that they have the same leading term, and then subtracting.

Equations

• p.cancelLeads q = Polynomial.C p.leadingCoeff * Polynomial.X ^ (p.natDegree - q.natDegree) * q - Polynomial.C q.leadingCoeff * Polynomial.X ^ (q.natDegree - p.natDegree) * p

@[simp]

theorem Polynomial.neg_cancelLeads {R : Type u_1} [Ring R] {p q : Polynomial R} : -p.cancelLeads q = q.cancelLeads p

theorem Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm {R : Type u_1} [Ring R] {p q : Polynomial R} (comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff) (h : p.natDegree ≤ q.natDegree) (hq : 0 < q.natDegree) : (p.cancelLeads q).natDegree < q.natDegree

theorem Polynomial.dvd_cancelLeads_of_dvd_of_dvd {R : Type u_1} [CommRing R] {p q r : Polynomial R} (pq : p ∣ q) (pr : p ∣ r) : p ∣ q.cancelLeads r

theorem Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree {R : Type u_1} [CommRing R] {p q : Polynomial R} (h : p.natDegree ≤ q.natDegree) (hq : 0 < q.natDegree) : (p.cancelLeads q).natDegree < q.natDegree