mathlib documentation


Cancel the leading terms of two polynomials #

Definition #

Main Results #

The degree of cancel_leads 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.cancel_leads {R : Type u_1} [ring R] (p q : polynomial R) :

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

theorem polynomial.neg_cancel_leads {R : Type u_1} [ring R] {p q : polynomial R} :
theorem polynomial.dvd_cancel_leads_of_dvd_of_dvd {R : Type u_1} [comm_ring R] {p q r : polynomial R} (pq : p q) (pr : p r) :