def Hex.CertificateSyntax.reifyPrimeFactorData (d : PrimeFactorData) : Lean.Expr

Reify a PrimeFactorData block as a constructor application over its reified prime, degree array, factor array, and nested Rabin certificates.

Equations

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

def Hex.CertificateSyntax.reifyDegreeObstruction (o : DegreeObstruction) : Lean.Expr

Reify a DegreeObstruction as a constructor application.

Equations

• Hex.CertificateSyntax.reifyDegreeObstruction o = Lean.mkApp2 (Lean.mkConst `Hex.DegreeObstruction.mk) (Lean.mkNatLit o.targetDegree) (Lean.mkNatLit o.primeIndex)

def Hex.CertificateSyntax.reifyCertificate (cert : ZPolyIrreducibilityCertificate) : Lean.Expr

Reify a full ZPolyIrreducibilityCertificate as a literal Expr.

Equations

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

def Hex.CertificateSyntax.reifyZPoly (f : ZPoly) : Lean.MetaM Lean.Expr

Reify a ZPoly as Hex.DensePoly.ofCoeffs #[…] with literal Int coefficients.

Equations

• Hex.CertificateSyntax.reifyZPoly f = Lean.Meta.mkAppM `Hex.DensePoly.ofCoeffs #[Hex.CertificateSyntax.arrayLit (Lean.mkConst `Int) (List.map Lean.toExpr (Hex.DensePoly.toArray f).toList)]

def Hex.CertificateSyntax.primeFactorDataData (d : PrimeFactorData) : Nat × List Nat × List (List Nat) × List (Nat × Nat × List (List Nat) × List (List Nat × List Nat))

Serialized view of a per-prime certificate block.

Equations

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

def Hex.CertificateSyntax.certificateData (cert : ZPolyIrreducibilityCertificate) : List (Nat × List Nat × List (List Nat) × List (Nat × Nat × List (List Nat) × List (List Nat × List Nat))) × List (Nat × Nat)

Serialized view of a full integer irreducibility certificate.

Equations

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