HepLean Documentation

Mathlib.Algebra.Polynomial.CancelLeads

Cancel the leading terms of two polynomials #

Definition #

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.

source
def Polynomial.cancelLeads {R : Type u_1} [Ring R] (p : Polynomial R) (q : Polynomial R) :
Polynomial R

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

Equations
  • p.cancelLeads q = Polynomial.C p.leadingCoeff * Polynomial.X ^ (p.natDegree - q.natDegree) * q - Polynomial.C q.leadingCoeff * Polynomial.X ^ (q.natDegree - p.natDegree) * p
Instances For
    source
    @[simp]
    theorem Polynomial.neg_cancelLeads {R : Type u_1} [Ring R] {p : Polynomial R} {q : Polynomial R} :
    -p.cancelLeads q = q.cancelLeads p
    source
    theorem Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm {R : Type u_1} [Ring R] {p : Polynomial R} {q : Polynomial R} (comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff) (h : p.natDegree ≤ q.natDegree) (hq : 0 < q.natDegree) :
    (p.cancelLeads q).natDegree < q.natDegree
    source
    theorem Polynomial.dvd_cancelLeads_of_dvd_of_dvd {R : Type u_1} [CommRing R] {p : Polynomial R} {q : Polynomial R} {r : Polynomial R} (pq : p ∣ q) (pr : p ∣ r) :
    p ∣ q.cancelLeads r
    source
    theorem Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree {R : Type u_1} [CommRing R] {p : Polynomial R} {q : Polynomial R} (h : p.natDegree ≤ q.natDegree) (hq : 0 < q.natDegree) :
    (p.cancelLeads q).natDegree < q.natDegree