structure Hex.FpPoly.Factored {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : Type

A certified irreducible factorization of f : FpPoly p: a scalar and a factor list (with repetition) whose product reconstructs f, every listed factor irreducible. Produced by the factor_poly elaborator with monic factors and the leading unit in scalar.

• scalar : ZMod64 p

  The unit scalar (the leading coefficient for nonzero f).

• factors : List (FpPoly p)

  The irreducible factors, with repetition (monic by generator convention).

• factors_mul : DensePoly.C self.scalar * self.factors.prod = f

  The scalar times the factor product reconstructs f.

• factors_irred (q : FpPoly p) : q ∈ self.factors → q.Irreducible

  Every listed factor is irreducible.