Cancel the leading terms of two polynomials #

Definition #

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.

def Polynomial.cancelLeads {R : Type u_1} [Ring R] (p : Polynomial R) (q : 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.

Instances For
    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) :