17.7. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexGFqMathlib connects it to Mathlib: for prime p, the executable field Hex.GFq is ring-isomorphic to Mathlib's GaloisField p n, with p ^ n elements.

def

HexGFqMathlib.GFq.equivGaloisField {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] [Fact (Nat.Prime p)]
  (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) :
  Hex.GFq p n h ≃+* GaloisField p n
HexGFqMathlib.GFq.equivGaloisField
  {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  [Fact (Nat.Prime p)]
  (h : Hex.Conway.SupportedEntry p n)
  (hn : n ≠ 0) :
  Hex.GFq p n h ≃+* GaloisField p n

Canonical GFq values are ring-equivalent to Mathlib's GaloisField with the same characteristic and extension degree.

theorem

HexGFqMathlib.GFq.fintype_card_eq_pow {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (h : Hex.Conway.SupportedEntry p n) :
  Fintype.card (Hex.GFq p n h) = p ^ n
HexGFqMathlib.GFq.fintype_card_eq_pow
  {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (h : Hex.Conway.SupportedEntry p n) :
  Fintype.card (Hex.GFq p n h) = p ^ n

Cardinality of canonical GFq p n as p ^ n.

theorem

HexGFqMathlib.GFq.card_eq_galoisField_card {p n : ℕ}
  [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] [Fact (Nat.Prime p)]
  (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) :
  Fintype.card (Hex.GFq p n h) = Nat.card (GaloisField p n)
HexGFqMathlib.GFq.card_eq_galoisField_card
  {p n : ℕ} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  [Fact (Nat.Prime p)]
  (h : Hex.Conway.SupportedEntry p n)
  (hn : n ≠ 0) :
  Fintype.card (Hex.GFq p n h) =
    Nat.card (GaloisField p n)

Canonical GFq and Mathlib's GaloisField have matching cardinalities.