hex

6.6. The Euclidean layer🔗

Division and gcd route through the dense representation, and the library makes no claim that they stay sparse: the cost is the dense cost at the degree plus the conversions. The one division that stays sparse is division by a monomial.

🔗def
Hex.SparsePoly.divModMonic.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] (s t : Hex.SparsePoly R)
  (ht : t.Monic) : Hex.SparsePoly R × Hex.SparsePoly R
Hex.SparsePoly.divModMonic.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R]
  (s t : Hex.SparsePoly R)
  (ht : t.Monic) :
  Hex.SparsePoly R × Hex.SparsePoly R

Divide by a monic divisor, through the dense representation: two toDense and two ofDense conversions around DensePoly.divModMonic.

🔗def
Hex.SparsePoly.divMod.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] (s t : Hex.SparsePoly R) :
  Hex.SparsePoly R × Hex.SparsePoly R
Hex.SparsePoly.divMod.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (s t : Hex.SparsePoly R) :
  Hex.SparsePoly R × Hex.SparsePoly R

Field-style division with remainder, through the dense representation.

🔗def
Hex.SparsePoly.gcd.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] (s t : Hex.SparsePoly R) :
  Hex.SparsePoly R
Hex.SparsePoly.gcd.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  (s t : Hex.SparsePoly R) :
  Hex.SparsePoly R

Euclidean gcd, through the dense representation: the dense cost at the degree, whatever the term count. A caller with a two-term input of degree 10^6 should expect this to cost what a dense gcd at degree 10^6 costs.

🔗def
Hex.SparsePoly.divExactMonic?.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] (s t : Hex.SparsePoly R)
  (ht : t.Monic) : Option (Hex.SparsePoly R)
Hex.SparsePoly.divExactMonic?.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R]
  (s t : Hex.SparsePoly R)
  (ht : t.Monic) :
  Option (Hex.SparsePoly R)

Exact division by a monic divisor: divModMonic with a zero-remainder test.

🔗def
Hex.SparsePoly.divMonomial?.{u} {R : Type u} [Zero R] [DecidableEq R]
  (s : Hex.SparsePoly R) (e : ℕ) : Option (Hex.SparsePoly R)
Hex.SparsePoly.divMonomial?.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  (s : Hex.SparsePoly R) (e : ℕ) :
  Option (Hex.SparsePoly R)

Divide by the monomial x^e, the one division that stays sparse: none unless every stored exponent is at least e, and otherwise a subtraction on each exponent, O(s) with no filtering.