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

## Equations

## 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 : 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 : Polynomial R}
{q : Polynomial R}
{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 : Polynomial R}
{q : Polynomial R}
(h : p.natDegree ≤ q.natDegree)
(hq : 0 < q.natDegree)
:

(p.cancelLeads q).natDegree < q.natDegree