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 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
12.
HexRealRoots: certified real-root isolation
12.1.
Introduction
12.2.
Mathlib-free execution
12.3.
The
isolate_roots
elaborator
12.4.
What the fields say
12.5.
Requesting tighter intervals
12.6.
Squarefreeness is invisible
12.7.
The Mathlib correspondence
12.8.
Cross-references
←
11.8. Cross-references
12.1. Introduction
→
12. HexRealRoots: certified real-root isolation
🔗
12.1.
Introduction
12.2.
Mathlib-free execution
12.3.
The
isolate_roots
elaborator
12.4.
What the fields say
12.5.
Requesting tighter intervals
12.6.
Squarefreeness is invisible
12.7.
The Mathlib correspondence
12.8.
Cross-references
←
11.8. Cross-references
12.1. Introduction
→