def Hex.Conway.luebeckConwayCoeffs? : Nat → Nat → Option (List Nat)

Imported coefficients in ascending degree order.

def Hex.Conway.luebeckConwayPolynomialOfCoeffs (p : Nat) [ZMod64.Bounds p] (coeffs : List Nat) : FpPoly p

Construct a polynomial from ascending coefficient representatives.

Equations

• Hex.Conway.luebeckConwayPolynomialOfCoeffs p coeffs = Hex.FpPoly.ofCoeffs (Array.map (fun (n : Nat) => Hex.ZMod64.ofNat p n) coeffs.toArray)

def Hex.Conway.luebeckConwayPolynomial? (p n : Nat) [ZMod64.Bounds p] : Option (FpPoly p)

Lookup an imported, verified polynomial.

Equations

• Hex.Conway.luebeckConwayPolynomial? p n = Option.map (Hex.Conway.luebeckConwayPolynomialOfCoeffs p) (Hex.Conway.luebeckConwayCoeffs? p n)

def Hex.Conway.supportedPairs : List (Nat × Nat)

Exact verified keys, in characteristic and degree order.

Equations

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