Cancel the leading terms of two polynomials #
Definition #
cancel_leads p q: the polynomial formed by multiplyingpandqby monomials so that they have the same leading term, and then subtracting.
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.
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
- p.cancel_leads q = ((⇑polynomial.C p.leading_coeff) * polynomial.X ^ (p.nat_degree - q.nat_degree)) * q - ((⇑polynomial.C q.leading_coeff) * polynomial.X ^ (q.nat_degree - p.nat_degree)) * p
@[simp]
theorem
polynomial.neg_cancel_leads
{R : Type u_1}
[ring R]
{p q : R[X]} :
-p.cancel_leads q = q.cancel_leads p
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) :
p ∣ q.cancel_leads r
theorem
polynomial.nat_degree_cancel_leads_lt_of_nat_degree_le_nat_degree
{R : Type u_1}
[comm_ring R]
[is_domain R]
{p q : R[X]}
(h : p.nat_degree ≤ q.nat_degree)
(hq : 0 < q.nat_degree) :
(p.cancel_leads q).nat_degree < q.nat_degree