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 #
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 : polynomial R} :
-p.cancel_leads q = q.cancel_leads p
theorem
polynomial.nat_degree_cancel_leads_lt_of_nat_degree_le_nat_degree_of_comm
{R : Type u_1}
[ring R]
{p q : polynomial R}
(comm : p.leading_coeff * q.leading_coeff = q.leading_coeff * p.leading_coeff)
(h : p.nat_degree ≤ q.nat_degree)
(hq : 0 < q.nat_degree) :
(p.cancel_leads q).nat_degree < q.nat_degree
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) :
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]
{p q : polynomial R}
(h : p.nat_degree ≤ q.nat_degree)
(hq : 0 < q.nat_degree) :
(p.cancel_leads q).nat_degree < q.nat_degree