structure Hex.FactoredPoly {R : Type u_1} [CommRing R] (P : Polynomial R) : Type u_1

A certified irreducible factorization of P : Polynomial R; Mathlib-side counterpart of FpPoly.Factored and ZPoly.Factored. Produced by the factor_poly elaborator via the Mathlib translation extensions.

• scalar : R

  The scalar factored out of P: over a finite field the leading unit of nonzero P; over ℤ the signed content.

• factors : List (Polynomial R)

  The irreducible factors, with repetition.

• factors_mul : Polynomial.C self.scalar * self.factors.prod = P

  The scalar times the factor product reconstructs P.

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

  Every listed factor is irreducible.

theorem HexBerlekampMathlib.nat_prime_of_hex {p : ℕ} (hp : Hex.Nat.Prime p) : Nat.Prime p

The Mathlib-free Hex.Nat.Prime witness yields Mathlib's Nat.Prime.

theorem HexBerlekampMathlib.toMathlibPolynomial_listProd {p : ℕ} [Hex.ZMod64.Bounds p] (l : List (Hex.FpPoly p)) : toMathlibPolynomial l.prod = (List.map toMathlibPolynomial l).prod

List products commute with the finite-field polynomial transport.

noncomputable def Hex.FactoredPoly.ofFp {p : ℕ} [inst : ZMod64.Bounds p] (P : Polynomial (ZMod p)) (f : FpPoly p) (s : ZMod64 p) (factors : List (FpPoly p)) (certified : List (FpPoly p × ZMod64 p × Berlekamp.IrreducibilityCertificate)) (hp : Nat.isPrimeTrial p = true) (hmul : (DensePoly.C s * factors.prod).beqCoeffs f = true) (hdeg : (factors.all fun (g : FpPoly p) => decide (0 < DensePoly.natDegree g)) = true) (hcheck : Berlekamp.checkIrredCover factors certified = true) (hP : HexPolyFpMathlib.toMathlibPolynomial f = P) : FactoredPoly P

One-shot assembler for the factor_poly extension on Polynomial (ZMod p): every certification slot is a Boolean check on reified literal data (filled by Eq.refl true in emitted terms), and hP is the parser-built translation equality tying the reified executable polynomial to the user's Mathlib polynomial.

Equations

• One or more equations did not get rendered due to their size.

theorem HexBerlekampMathlib.irreducible_ofFp {p : ℕ} [Hex.ZMod64.Bounds p] (P : Polynomial (ZMod p)) (f m : Hex.FpPoly p) (c : Hex.ZMod64 p) (cert : Hex.Berlekamp.IrreducibilityCertificate) (hp : Hex.Nat.isPrimeTrial p = true) (hc : decide (c = 0) = false) (hfm : (Hex.DensePoly.scale c m).beqCoeffs f = true) (hcheck : Hex.Berlekamp.checkMonicCert m cert = true) (hdeg : decide (0 < Hex.DensePoly.natDegree f) = true) (hP : toMathlibPolynomial f = P) : Irreducible P

Kernel-decidable irreducibility endpoint for the irreducibility extension on Polynomial (ZMod p): the executable side is Berlekamp.irreducible_of_checkMonicCert_scale on reified literals, the positive degree transports the statement out of the vacuous-constant regime, and hP is the parser-built translation equality.