hex

24.2. The executable API🔗

The public chain records its normalized inputs, every nonzero remainder, and the terminal principal-subresultant scalar. The scalar is separate because a defective degree drop can change the exact resultant without changing the last nonzero polynomial.

🔗structure
Hex.PRSResult.{u} (R : Type u) [Zero R] [DecidableEq R] : Type u
Hex.PRSResult.{u} (R : Type u) [Zero R]
  [DecidableEq R] : Type u

Executable result of a degree-ordered Brown PRS run.

scale belongs to the ordered chain. In particular, subresultantRun does not record whether it swapped its arguments, so this structure alone is not a caller-order-sensitive resultant; use resultant for that value.

Constructor

Hex.PRSResult.mk.{u}

Fields

chain : Array (Hex.DensePoly R)

Brown's nonzero G₁, …, Gₖ, excluding the generated terminal zero.

scale : R

Corrected terminal principal-subresultant scalar hₖ.

🔗def
Hex.DensePoly.subresultantChain.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) : Array (Hex.DensePoly R)
Hex.DensePoly.subresultantChain.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  (f g : Hex.DensePoly R) :
  Array (Hex.DensePoly R)

Brown's nonzero subresultant pseudo-remainder sequence.