hex

17.4. Using the executable API🔗

open Hex local instance boundsFive : ZMod64.Bounds 5 := ⟨⊢ 0 < 5 All goals completed! 🐙, ⊢ 5 < 2 ^ 31 All goals completed! 🐙⟩ def f : FpPoly 5 := #p[1, 0, 1] Hex.Berlekamp.berlekampFactor {p : ℕ} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) [ZMod64.PrimeModulus p] : Berlekamp.Factorization p#check Berlekamp.berlekampFactor Hex.Berlekamp.rabinTest {p : ℕ} [ZMod64.Bounds p] (f : FpPoly p) (hmonic : DensePoly.Monic f) : Bool#check Berlekamp.rabinTest

The ordinary umbrella contains the executable factorization and the certificate-backed factor_poly and irreducibility syntax for FpPoly p. Importing HexBerlekampMathlib adds the corresponding surface for Polynomial (ZMod p).