Documentation

HexGFqMathlib.GF2q

source
@[simp]
theorem Hex.GF2q.modulusFpPoly_eq_conway {n : ℕ} [h : GFq.PackedGF2Entry n] :
HexGF2Mathlib.GF2n.modulusFpPoly = GFq.modulus GFq.PackedGF2Entry.entry

The packed GF2n modulus, transported to FpPoly 2, is the Conway polynomial selected for the same committed packed entry.

source
def Hex.GF2q.equivGFq {n : ℕ} [h : GFq.PackedGF2Entry n] :
GF2q n ≃+* GFq 2 n GFq.PackedGF2Entry.entry

The optimized packed binary Conway field is ring-equivalent to the generic canonical Conway field over p = 2.

This is the composition the hex-gfq-mathlib SPEC describes: the packed side corresponds to the generic quotient field over the same modulus (HexGF2Mathlib.GF2n.equiv), and that modulus is the Conway polynomial for (2, n) (Hex.GF2q.genericField_eq_conway). Both factors are Mathlib RingEquivs, so the composition is just trans.

Equations
Instances For
    source
    noncomputable def Hex.GF2q.equivGaloisField {n : ℕ} [h : GFq.PackedGF2Entry n] :
    GF2q n ≃+* GaloisField 2 n

    The optimized packed binary Conway field is ring-equivalent to Mathlib's GaloisField of the same order.

    This is the composite the hex-gfq-mathlib SPEC describes: Hex.GF2q.equivGFq carries the packed representation onto the generic one, and HexGFqMathlib.GFq.equivGaloisField carries that onto Mathlib. It is the statement a user reaches for when they want to discharge a GaloisField 2 n goal by computing in the packed representation.

    Noncomputable because the second leg goes through FiniteField.ringEquivOfCardEq, which chooses an isomorphism rather than constructing one; Hex.GF2q.equivGFq, the leg that does the packing work, is computable.

    Equations
    Instances For