hex

12.4. Division, gcd, and extended gcd🔗

Long division over F₂ needs no coefficient inversion (the leading coefficient of any nonzero polynomial is already 1), so the packed representation supports a direct shift-and-XOR division. Hex.GF2Poly.divMod returns the quotient and remainder, with the Div and Mod instances projecting out each component.

🔗def
Hex.GF2Poly.divMod (p q : Hex.GF2Poly) : Hex.GF2Poly × Hex.GF2Poly
Hex.GF2Poly.divMod (p q : Hex.GF2Poly) :
  Hex.GF2Poly × Hex.GF2Poly

Polynomial long division over GF(2). Division by 0 returns (0, p).

The Euclidean algorithm built on divMod gives both the plain gcd and its extended form, which additionally returns the Bézout cofactors.

🔗def
Hex.GF2Poly.gcd (p q : Hex.GF2Poly) : Hex.GF2Poly
Hex.GF2Poly.gcd (p q : Hex.GF2Poly) :
  Hex.GF2Poly

Polynomial gcd over packed GF(2).

🔗def
Hex.GF2Poly.xgcd (p q : Hex.GF2Poly) : Hex.GF2Poly.XGCDResult
Hex.GF2Poly.xgcd (p q : Hex.GF2Poly) :
  Hex.GF2Poly.XGCDResult

Extended gcd for packed GF(2) polynomials, returning the gcd together with Bezout coefficients.

The extended result bundles the gcd together with the two cofactors satisfying left · a + right · b = gcd.

🔗structure
Hex.GF2Poly.XGCDResult : Type
Hex.GF2Poly.XGCDResult : Type

Result package for the packed extended Euclidean algorithm.

Constructor

Hex.GF2Poly.XGCDResult.mk

Fields

gcd : Hex.GF2Poly

The gcd of the two input polynomials.

left : Hex.GF2Poly

Bezout cofactor multiplying the first input: left * a + right * b = gcd.

right : Hex.GF2Poly

Bezout cofactor multiplying the second input: left * a + right * b = gcd.