# 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.

source
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

Instances For

source
@[simp]
theorem Polynomial.neg_cancelLeads {R : Type u_1} [Ring R] {p q : Polynomial R} :
-p.cancelLeads q = q.cancelLeads p
source
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
source
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
source
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