Verified computational algebra in Lean 4: an aggregator for the released
hex libraries.
Requiring this package pulls in the whole released hex-lll-mathlib closure
at a single coherent pinned set. The Mathlib-free computational libraries
(what used to be a single HexMatrix is now split into a matrix layer and
the row-reduction, determinant, and Bareiss libraries built on it):
| Library | Repo |
|---|---|
HexBasic |
hex-basic |
HexMatrix |
hex-matrix |
HexRowReduce |
hex-row-reduce |
HexDeterminant |
hex-determinant |
HexBareiss |
hex-bareiss |
HexGramSchmidt |
hex-gram-schmidt |
HexLLL |
hex-lll |
and their Mathlib correspondence layers:
| Library | Repo |
|---|---|
HexMatrixMathlib |
hex-matrix-mathlib |
HexRowReduceMathlib |
hex-row-reduce-mathlib |
HexDeterminantMathlib |
hex-determinant-mathlib |
HexBareissMathlib |
hex-bareiss-mathlib |
HexGramSchmidtMathlib |
hex-gram-schmidt-mathlib |
HexLLLMathlib |
hex-lll-mathlib |
require hex from git "https://github.com/kim-em/hex.git" @ "<rev>"
To depend on just the Mathlib-free LLL, require
hex-lll directly.
Development of the full project (including unreleased libraries) happens in the
hex-dev monorepo.