mathlib documentation

data.polynomial.cancel_leads

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 : R[X]) :

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

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