hex
hex
Table of Contents
1.
HexBasic: shared dependency-free utilities
2.
HexArith: low-level arithmetic foundations
3.
HexPrimality: certified primality at scale
4.
HexECPP: bounded elliptic-curve certificates
5.
HexPoly: normalized dense polynomials
6.
HexMvPoly: executable sparse multivariate polynomials
7.
HexSparsePoly: sparse univariate polynomials
8.
HexModArith: machine-word modular arithmetic
9.
HexPolyFp: prime-field dense polynomials
10.
HexPolyZ: integer dense polynomials
11.
HexGFqRing: executable Fₚ quotient ring
12.
HexHensel: executable Hensel lifting
13.
HexRoots: certified complex-root isolation
14.
HexRealRoots: certified real-root isolation
15.
HexRCF: a decision procedure for univariate real arithmetic
16.
HexMatrix: dense matrices and arithmetic
17.
HexRowReduce: Gauss-Jordan reduction, span, and nullspace
18.
HexBerlekamp: factorization over finite fields
19.
HexGF2: packed GF(2) polynomials and GF(2ⁿ) fields
20.
HexGFqField: executable GF(pⁿ)
21.
HexConway: verified Conway-polynomial lookup
22.
HexGFq: canonical finite-field constructors
23.
HexDeterminant: the Leibniz determinant and cofactor theory
24.
HexBareiss: the fraction-free determinant
25.
HexResultant: subresultants and discriminants
26.
HexGramSchmidt: Gram-Schmidt orthogonalization
27.
HexLLL: lattice basis reduction
28.
HexBerlekampZassenhaus: factorization over the integers
29.
factor_poly
and
irreducibility
: certified factoring
30.
HexNumberField: exact algebraic numbers
31.
HexNumberFieldTower: successive algebraic extensions
32.
HexPermGroup: checked finite permutation groups
33.
HexGraphIso: coloured graph canonical labelling
34.
The
nauty
canonical labelling algorithm
35.
Tutorials
36.
Draft sections for unreleased libraries
4.
HexECPP: bounded elliptic-curve certificates
4.1.
Introduction
4.2.
Certificates and subject binding
4.3.
Supplied PARI conversion
4.4.
Bounded native production
4.5.
The Mathlib correspondence
←
3.11. Cross-references
4.1. Introduction
→
4. HexECPP: bounded elliptic-curve certificates
🔗
4.1.
Introduction
4.2.
Certificates and subject binding
4.3.
Supplied PARI conversion
4.4.
Bounded native production
4.5.
The Mathlib correspondence
←
3.11. Cross-references
4.1. Introduction
→