Cancel the leading terms of two polynomials #
Definition #
cancelLeads p q
: the polynomial formed by multiplyingp
andq
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.dvd_cancelLeads_of_dvd_of_dvd
{R : Type u_1}
[CommRing R]
{p q r : Polynomial R}
(pq : p ∣ q)
(pr : p ∣ r)
: