leanproverhex-lll

LLL lattice reduction for the hex project (optional fpLLL FFI). Mathlib-free.
Displaying 1-2 of 2 packages depending on leanprover/hex-lll
Sort by

  1. leanprover/hexuses4691e24

    Verified computational algebra in Lean 4: aggregator for the released hex libraries

  2. JJYYY-JJY/NormalFormsusesa73f188

    Executable Hermite and Smith Normal Forms in Lean 4 over Euclidean Domains, with a PID bridge to mathlib.