mathlib3 documentation

data.polynomial.cancel_leads

Cancel the leading terms of two polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Equations
@[simp]
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) :