9.6. Euclidean operations🔗

Over a field the dense representation supports division with remainder, quotient and remainder operators, and gcd. The entry points are the leading coefficient and the monic predicate.

def

Hex.DensePoly.leadingCoeff.{u} {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : R
Hex.DensePoly.leadingCoeff.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : R

The leading coefficient, or 0 for the zero polynomial.

def

Hex.DensePoly.Monic.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  (p : Hex.DensePoly R) : Prop
Hex.DensePoly.Monic.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R]
  (p : Hex.DensePoly R) : Prop

A polynomial is monic when its leading coefficient is 1.

theorem

Hex.DensePoly.monic_iff_leadingCoeff_eq_one.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] {p : Hex.DensePoly R} :
  p.Monic ↔ p.leadingCoeff = 1
Hex.DensePoly.monic_iff_leadingCoeff_eq_one.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] {p : Hex.DensePoly R} :
  p.Monic ↔ p.leadingCoeff = 1

Characterization of Monic by the leading coefficient equation.

Division has two flavours. Hex.DensePoly.divModMonic divides by a monic divisor over any commutative ring. No division of coefficients is needed because the leading coefficient is 1. Hex.DensePoly.divMod is the field version: it scales by the inverse of the divisor's leading coefficient and so requires a Div on the coefficient type.

def

Hex.DensePoly.divModMonic.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] (p q : Hex.DensePoly R)
  (_hmonic : q.Monic) : Hex.DensePoly R × Hex.DensePoly R
Hex.DensePoly.divModMonic.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] (p q : Hex.DensePoly R)
  (_hmonic : q.Monic) :
  Hex.DensePoly R × Hex.DensePoly R

Divide by a monic polynomial. The remainder has degree below the divisor whenever the fuel is sufficient, which is the case for normalized dense polynomials.

def

Hex.DensePoly.divMod.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] (p q : Hex.DensePoly R) :
  Hex.DensePoly R × Hex.DensePoly R
Hex.DensePoly.divMod.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly R × Hex.DensePoly R

Polynomial division with remainder over a field.

The Div, Mod, and Dvd instances expose the field quotient and remainder as p / q, p % q, and q ∣ p, and the extended algorithm returns the gcd with its Bezout coefficients.

def

Hex.DensePoly.div.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] (p q : Hex.DensePoly R) :
  Hex.DensePoly R
Hex.DensePoly.div.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly R

Quotient from polynomial long division over a field.

def

Hex.DensePoly.mod.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] (p q : Hex.DensePoly R) :
  Hex.DensePoly R
Hex.DensePoly.mod.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly R

Remainder from polynomial long division over a field.

def

Hex.DensePoly.modByMonic.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] (p q : Hex.DensePoly R)
  (hmonic : q.Monic) : Hex.DensePoly R
Hex.DensePoly.modByMonic.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] (p q : Hex.DensePoly R)
  (hmonic : q.Monic) : Hex.DensePoly R

Remainder from long division by a monic polynomial over a commutative ring.

def

Hex.DensePoly.gcd.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] (p q : Hex.DensePoly R) :
  Hex.DensePoly R
Hex.DensePoly.gcd.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly R

Polynomial gcd over a field. Computed by the plain remainder sequence (gcdAux), not the extended algorithm: the gcd value is independent of the Bezout coefficients, and computing them costs an extra polynomial multiplication per step (O(deg³) vs O(deg²)). xgcd stays available for callers that genuinely need Bezout coefficients.

def

Hex.DensePoly.xgcd.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] (p q : Hex.DensePoly R) :
  Hex.DensePoly.XGCDResult R
Hex.DensePoly.xgcd.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (p q : Hex.DensePoly R) :
  Hex.DensePoly.XGCDResult R

Extended gcd over a field, returning the gcd together with Bezout coefficients.

9.6.1. Worked example: division over the rationals🔗

This block works over DensePoly Rat. It divides x² - 1 by x - 1, reads off the quotient and remainder, checks the Euclidean reconstruction, and computes a gcd.

open Hex Hex.DensePoly

namespace HexPolyChapterEuclid

-- p = x² - 1, q = x - 1
private def p : DensePoly Rat := ofCoeffs #[-1, 0, 1]
private def q : DensePoly Rat := ofCoeffs #[-1, 1]

-- x² - 1 = (x - 1)(x + 1), so the division is exact.
-- Quotient x + 1, remainder 0.
#guard (divMod p q).1.toArray.toList = [1, 1]
#guard (divMod p q).2 = (0 : DensePoly Rat)
#guard (p / q).toArray.toList = [1, 1]
#guard p % q = (0 : DensePoly Rat)

-- Euclidean reconstruction: (p / q) · q + (p % q) = p.
#guard (p / q) * q + (p % q) = p

-- q is monic, so it also divides p through the
-- ring-only path.
#guard q.leadingCoeff = 1
#guard modByMonic p q (by⊢ q.Monic rflAll goals completed! 🐙) = (0 : DensePoly Rat)

-- gcd(x² - 1, x + 1) = x + 1: a monic gcd.
#guard gcd p (ofCoeffs #[1, 1]) = ofCoeffs #[1, 1]

end HexPolyChapterEuclid