hex
hex
Table of Contents
1.
HexBasic: shared dependency-free utilities
2.
HexArith: low-level arithmetic foundations
3.
HexPoly: normalized dense polynomials
4.
HexMvPoly: executable sparse multivariate polynomials
5.
HexSparsePoly: sparse univariate polynomials
6.
HexModArith: machine-word modular arithmetic
7.
HexPolyFp: prime-field dense polynomials
8.
HexPolyZ: integer dense polynomials
9.
HexGFqRing: executable Fₚ quotient ring
10.
HexHensel: executable Hensel lifting
11.
HexRoots: certified complex-root isolation
12.
HexRealRoots: certified real-root isolation
13.
HexMatrix: dense matrices and arithmetic
14.
HexRowReduce: Gauss-Jordan reduction, span, and nullspace
15.
HexBerlekamp: factorization over finite fields
16.
HexGF2: packed GF(2) polynomials and GF(2ⁿ) fields
17.
HexGFqField: executable GF(pⁿ)
18.
HexConway: Tier 1 Conway-polynomial lookup
19.
HexGFq: canonical finite-field constructors
20.
HexDeterminant: the Leibniz determinant and cofactor theory
21.
HexBareiss: the fraction-free integer determinant
22.
HexGramSchmidt: Gram-Schmidt orthogonalization
23.
HexLLL: lattice basis reduction
24.
HexBerlekampZassenhaus: factorization over the integers
25.
factor_poly
and
irreducibility
: certified factoring
26.
Tutorials
27.
Draft sections for unreleased libraries
13.
HexMatrix: dense matrices and arithmetic
13.1.
Introduction
13.2.
The dense matrix type
13.3.
Arithmetic worked example
13.4.
Entry, row, and column lemmas
13.5.
Elementary operations
13.6.
Worked example
13.7.
The Mathlib correspondence
13.8.
Cross-references
←
12.7. Cross-references
13.1. Introduction
→
13. HexMatrix: dense matrices and arithmetic
🔗
13.1.
Introduction
13.2.
The dense matrix type
13.3.
Arithmetic worked example
13.4.
Entry, row, and column lemmas
13.5.
Elementary operations
13.6.
Worked example
13.7.
The Mathlib correspondence
13.8.
Cross-references
←
12.7. Cross-references
13.1. Introduction
→