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

`cancelLeads p q`

is formed by multiplying `p`

and `q`

by monomials so that they
have the same leading term, and then subtracting.

## Instances For

@[simp]

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

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

p ∣ Polynomial.cancelLeads q r

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