Documentation

Mathlib.Data.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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Polynomial.neg_cancelLeads {R : Type u_1} [Ring R] {p : Polynomial R} {q : Polynomial R} :
    -Polynomial.cancelLeads p q = Polynomial.cancelLeads q 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 : Polynomial.leadingCoeff p * Polynomial.leadingCoeff q = Polynomial.leadingCoeff q * Polynomial.leadingCoeff p) (h : Polynomial.natDegree p ≤ Polynomial.natDegree q) (hq : 0 < Polynomial.natDegree q) :
    Polynomial.natDegree (Polynomial.cancelLeads p q) < Polynomial.natDegree q
    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 ∣ Polynomial.cancelLeads q r
    source
    theorem Polynomial.natDegree_cancelLeads_lt_of_natDegree_le_natDegree {R : Type u_1} [CommRing R] {p : Polynomial R} {q : Polynomial R} (h : Polynomial.natDegree p ≤ Polynomial.natDegree q) (hq : 0 < Polynomial.natDegree q) :
    Polynomial.natDegree (Polynomial.cancelLeads p q) < Polynomial.natDegree q