structure Hex.ZPoly.Factored (f : ZPoly) : Type

A certified irreducible factorization of f : ZPoly: a scalar (the signed content) and a factor list (with repetition) whose product reconstructs f, every listed factor irreducible in the element sense of ℤ[X]. Produced by the factor_poly elaborator with primitive positive-leading-coefficient factors.

• scalar : Int

  The scalar (the signed content for nonzero f).

• factors : List ZPoly

  The irreducible factors, with repetition (primitive, positive leading coefficient, by generator convention).

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

  The scalar times the factor product reconstructs f.

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

  Every listed factor is irreducible.