hex

14.2. Quotient types🔗

The two primitive notions are Hex.GFqRing.reduceMod (canonical remainder modulo f) and Hex.GFqRing.PolyQuotient (the subtype of reduced representatives).

🔗def
Hex.GFqRing.reduceMod {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) : Hex.FpPoly p → Hex.FpPoly p
Hex.GFqRing.reduceMod {p : Nat}
  [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  Hex.FpPoly p → Hex.FpPoly p

Canonical remainder reduction modulo f, using the existing division surface.

🔗def
Hex.GFqRing.IsReduced {p : Nat} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) : Prop
Hex.GFqRing.IsReduced {p : Nat}
  [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) : Prop

Polynomials already known to be canonical representatives modulo f.

🔗def
Hex.GFqRing.PolyQuotient {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (_hf : 0 < f.degree) : Type
Hex.GFqRing.PolyQuotient {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (_hf : 0 < f.degree) : Type

Executable quotient elements represented by canonical reduced polynomials.

Two further definitions are the main entry points: the smart constructor Hex.GFqRing.ofPoly and the projection Hex.GFqRing.repr. Callers never manage reduction by hand: ofPoly runs the canonical reduction and repr reads back the stored representative.

🔗def
Hex.GFqRing.ofPoly {p : Nat} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (g : Hex.FpPoly p) : Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.ofPoly {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree) (g : Hex.FpPoly p) :
  Hex.GFqRing.PolyQuotient f hf

Inject a polynomial into the quotient by reducing it modulo f.

🔗def
Hex.GFqRing.repr {p : Nat} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree} (x : Hex.GFqRing.PolyQuotient f hf) : Hex.FpPoly p
Hex.GFqRing.repr {p : Nat}
  [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p}
  {hf : 0 < f.degree}
  (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.FpPoly p

Project a quotient element to its canonical polynomial representative.