hex

8.6. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexPolyFpMathlib is the companion that connects it to Mathlib, and this section is where that library is documented. It is the crossing point for the whole executable polynomial tower, not only for this chapter's library: below it a reader is in Hex's own Hex.DensePoly over Hex.ZMod64, and on the far side of it in Mathlib's Polynomial (ZMod p).

🔗def
HexPolyFpMathlib.fpPolyEquiv {p : ℕ} [Hex.ZMod64.Bounds p] :
  Hex.FpPoly p ≃+* Polynomial (ZMod p)
HexPolyFpMathlib.fpPolyEquiv {p : ℕ}
  [Hex.ZMod64.Bounds p] :
  Hex.FpPoly p ≃+* Polynomial (ZMod p)

The executable finite-field polynomial representation is ring-equivalent to Mathlib polynomials over ZMod p.

The equivalence asks only for Hex.ZMod64.Bounds, not for primality. FpPoly p is a commutative ring for every admissible modulus, meaning every p with 0 < p and p < 2 ^ 31, which is what that class requires; Polynomial (ZMod p) is one for any p at all; and nothing in the correspondence divides. So there is no reason to demand more of p than the representation itself does. Primality enters at exactly one declaration, and as an explicit hypothesis.

🔗theorem
HexPolyFpMathlib.primeModulus_of_fact (p : ℕ) [Fact (Nat.Prime p)] :
  Hex.ZMod64.PrimeModulus p
HexPolyFpMathlib.primeModulus_of_fact
  (p : ℕ) [Fact (Nat.Prime p)] :
  Hex.ZMod64.PrimeModulus p

The Mathlib primality fact yields the executable prime-modulus witness, so executable field-dependent lemmas (gcd/Bezout, modular division) become available in the Mathlib transport layer.

That is the door from Mathlib's Fact (Nat.Prime p) to the executable Hex.ZMod64.PrimeModulus witness that the field-dependent operations require: coefficient inversion, the Bezout gcd, and modular division, and everything in The quotient by a modulus built on them. A caller who is already working in Mathlib supplies the Fact and gets the witness; a caller staying on the executable side never needs the Fact.

8.6.1. The forward map🔗

Downstream statements are written against a named forward map rather than against the equivalence, so that a goal about an executable polynomial's Mathlib image carries no RingEquiv coercion.

🔗def
HexPolyFpMathlib.toMathlibPolynomial {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) : Polynomial (ZMod p)
HexPolyFpMathlib.toMathlibPolynomial
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) : Polynomial (ZMod p)

Interpret an executable FpPoly p as a Mathlib polynomial over ZMod p.

🔗theorem
HexPolyFpMathlib.coeff_toMathlibPolynomial {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (n : ℕ) :
  (HexPolyFpMathlib.toMathlibPolynomial f).coeff n =
    HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff f n)
HexPolyFpMathlib.coeff_toMathlibPolynomial
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (n : ℕ) :
  (HexPolyFpMathlib.toMathlibPolynomial
          f).coeff
      n =
    HexModArithMathlib.ZMod64.toZMod
      (Hex.DensePoly.coeff f n)

Coefficients are preserved by the equivalence with Mathlib polynomials.

🔗theorem
HexPolyFpMathlib.coeff_polynomialToFpPoly {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Polynomial (ZMod p)) (n : ℕ) :
  Hex.DensePoly.coeff (HexPolyFpMathlib.polynomialToFpPoly f) n =
    HexModArithMathlib.ZMod64.ofZMod (f.coeff n)
HexPolyFpMathlib.coeff_polynomialToFpPoly
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Polynomial (ZMod p)) (n : ℕ) :
  Hex.DensePoly.coeff
      (HexPolyFpMathlib.polynomialToFpPoly
        f)
      n =
    HexModArithMathlib.ZMod64.ofZMod
      (f.coeff n)

Rebuilding a Mathlib polynomial preserves coefficients, transported back through the ZMod64 equivalence.

These coefficient lemmas are the normal forms for the two directions of the correspondence. They let downstream proofs cross the equivalence without unfolding either representation.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_monic {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  Hex.DensePoly.Monic f → (HexPolyFpMathlib.toMathlibPolynomial f).Monic
HexPolyFpMathlib.toMathlibPolynomial_monic
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  Hex.DensePoly.Monic f →
    (HexPolyFpMathlib.toMathlibPolynomial
        f).Monic

Monicity of executable finite-field polynomials transfers to Mathlib.

No nontriviality hypothesis is required: when ZMod p is trivial every polynomial is monic, and otherwise the executable leading coefficient 1 transports to the Mathlib leading coefficient 1.

Monicity is the hypothesis the executable Euclidean operations carry, so transporting it is what lets a Mathlib-side argument apply Polynomial.Monic lemmas to a polynomial that came out of Hex.FpPoly.modByMonic or out of the square-free decomposition.

🔗theorem
HexPolyFpMathlib.natDegree_toMathlibPolynomial {p : ℕ}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) :
  (HexPolyFpMathlib.toMathlibPolynomial f).natDegree =
    Hex.DensePoly.natDegree f
HexPolyFpMathlib.natDegree_toMathlibPolynomial
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  (HexPolyFpMathlib.toMathlibPolynomial
        f).natDegree =
    Hex.DensePoly.natDegree f

The executable degree transports to Mathlib's natDegree, with the zero polynomial mapping to degree 0. No nontriviality hypothesis is needed: in the trivial ring every transported polynomial is zero and every executable coefficient is zero as well.

🔗theorem
HexPolyFpMathlib.leadingCoeff_toMathlibPolynomial {p : ℕ}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) :
  (HexPolyFpMathlib.toMathlibPolynomial f).leadingCoeff =
    HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.leadingCoeff f)
HexPolyFpMathlib.leadingCoeff_toMathlibPolynomial
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  (HexPolyFpMathlib.toMathlibPolynomial
        f).leadingCoeff =
    HexModArithMathlib.ZMod64.toZMod
      (Hex.DensePoly.leadingCoeff f)

The executable leading coefficient transports through toZMod to Mathlib's leading coefficient.

8.6.2. The transport family🔗

The forward map is a ring equivalence, so each of the following follows from it. They are stated anyway: a caller reaching for one of them should not have to rediscover which RingEquiv lemma to compose, and the rewrite-friendly form is what the finite-field proofs actually use.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_add {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial (f + g) =
    HexPolyFpMathlib.toMathlibPolynomial f +
      HexPolyFpMathlib.toMathlibPolynomial g
HexPolyFpMathlib.toMathlibPolynomial_add
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial
      (f + g) =
    HexPolyFpMathlib.toMathlibPolynomial
        f +
      HexPolyFpMathlib.toMathlibPolynomial
        g

Addition commutes with the finite-field polynomial transport.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_sub {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial (f - g) =
    HexPolyFpMathlib.toMathlibPolynomial f -
      HexPolyFpMathlib.toMathlibPolynomial g
HexPolyFpMathlib.toMathlibPolynomial_sub
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial
      (f - g) =
    HexPolyFpMathlib.toMathlibPolynomial
        f -
      HexPolyFpMathlib.toMathlibPolynomial
        g

Subtraction commutes with the finite-field polynomial transport.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_neg {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial (-f) =
    -HexPolyFpMathlib.toMathlibPolynomial f
HexPolyFpMathlib.toMathlibPolynomial_neg
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial
      (-f) =
    -HexPolyFpMathlib.toMathlibPolynomial
        f

Negation commutes with the finite-field polynomial transport.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_mul {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial (f * g) =
    HexPolyFpMathlib.toMathlibPolynomial f *
      HexPolyFpMathlib.toMathlibPolynomial g
HexPolyFpMathlib.toMathlibPolynomial_mul
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial
      (f * g) =
    HexPolyFpMathlib.toMathlibPolynomial
        f *
      HexPolyFpMathlib.toMathlibPolynomial
        g

Multiplication commutes with the finite-field polynomial transport.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_derivative {p : ℕ}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial (Hex.DensePoly.derivative f) =
    Polynomial.derivative (HexPolyFpMathlib.toMathlibPolynomial f)
HexPolyFpMathlib.toMathlibPolynomial_derivative
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial
      (Hex.DensePoly.derivative f) =
    Polynomial.derivative
      (HexPolyFpMathlib.toMathlibPolynomial
        f)

Formal derivatives commute with the finite-field polynomial transport.

The derivative is the one that does not come free from the ring structure; it is proved coefficientwise. It is also the one the square-free correctness arguments need, since Yun's algorithm is stated in terms of the gcd of a polynomial with its derivative.

The generators transport too, so a Mathlib-side computation can be rewritten all the way down to X and constants.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_C {p : ℕ} [Hex.ZMod64.Bounds p]
  (c : Hex.ZMod64 p) :
  HexPolyFpMathlib.toMathlibPolynomial (Hex.DensePoly.C c) =
    Polynomial.C (HexModArithMathlib.ZMod64.toZMod c)
HexPolyFpMathlib.toMathlibPolynomial_C
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (c : Hex.ZMod64 p) :
  HexPolyFpMathlib.toMathlibPolynomial
      (Hex.DensePoly.C c) =
    Polynomial.C
      (HexModArithMathlib.ZMod64.toZMod c)

The constant executable polynomial transports to the Mathlib constant.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_X {p : ℕ} [Hex.ZMod64.Bounds p] :
  HexPolyFpMathlib.toMathlibPolynomial Hex.FpPoly.X = Polynomial.X
HexPolyFpMathlib.toMathlibPolynomial_X
  {p : ℕ} [Hex.ZMod64.Bounds p] :
  HexPolyFpMathlib.toMathlibPolynomial
      Hex.FpPoly.X =
    Polynomial.X

The executable indeterminate transports to Mathlib's X.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_monomial {p : ℕ}
  [Hex.ZMod64.Bounds p] (m : ℕ) (c : Hex.ZMod64 p) :
  HexPolyFpMathlib.toMathlibPolynomial (Hex.DensePoly.monomial m c) =
    (Polynomial.monomial m) (HexModArithMathlib.ZMod64.toZMod c)
HexPolyFpMathlib.toMathlibPolynomial_monomial
  {p : ℕ} [Hex.ZMod64.Bounds p] (m : ℕ)
  (c : Hex.ZMod64 p) :
  HexPolyFpMathlib.toMathlibPolynomial
      (Hex.DensePoly.monomial m c) =
    (Polynomial.monomial m)
      (HexModArithMathlib.ZMod64.toZMod c)

An executable monomial transports to the corresponding Mathlib monomial.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_monomial_one {p : ℕ}
  [Hex.ZMod64.Bounds p] (m : ℕ) :
  HexPolyFpMathlib.toMathlibPolynomial (Hex.DensePoly.monomial m 1) =
    Polynomial.X ^ m
HexPolyFpMathlib.toMathlibPolynomial_monomial_one
  {p : ℕ} [Hex.ZMod64.Bounds p] (m : ℕ) :
  HexPolyFpMathlib.toMathlibPolynomial
      (Hex.DensePoly.monomial m 1) =
    Polynomial.X ^ m

The monic monomial X^m transports to X^m over ZMod p.

The eval₂ theorem exposes Mathlib evaluation as the finite coefficient sum represented by the executable polynomial. Horner composition has a direct operation-correspondence theorem, so consumers need not repeat its polynomial induction.

🔗theorem
HexPolyFpMathlib.eval₂_toMathlibPolynomial.{u_1} {p : ℕ}
  [Hex.ZMod64.Bounds p] {S : Type u_1} [Semiring S] (h : ZMod p →+* S)
  (f : Hex.FpPoly p) (x : S) :
  Polynomial.eval₂ h x (HexPolyFpMathlib.toMathlibPolynomial f) =
    ∑ i ∈ Finset.range (Hex.DensePoly.size f),
      h (HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff f i)) *
        x ^ i
HexPolyFpMathlib.eval₂_toMathlibPolynomial.{u_1}
  {p : ℕ} [Hex.ZMod64.Bounds p]
  {S : Type u_1} [Semiring S]
  (h : ZMod p →+* S) (f : Hex.FpPoly p)
  (x : S) :
  Polynomial.eval₂ h x
      (HexPolyFpMathlib.toMathlibPolynomial
        f) =
    ∑
      i ∈
        Finset.range
          (Hex.DensePoly.size f),
      h
          (HexModArithMathlib.ZMod64.toZMod
            (Hex.DensePoly.coeff f i)) *
        x ^ i

Evaluation of a transported polynomial is its degree-indexed coefficient sum after transporting each executable coefficient through toZMod.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_compose {p : ℕ}
  [Hex.ZMod64.Bounds p] (f g : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial (Hex.DensePoly.compose f g) =
    (HexPolyFpMathlib.toMathlibPolynomial f).comp
      (HexPolyFpMathlib.toMathlibPolynomial g)
HexPolyFpMathlib.toMathlibPolynomial_compose
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) :
  HexPolyFpMathlib.toMathlibPolynomial
      (Hex.DensePoly.compose f g) =
    (HexPolyFpMathlib.toMathlibPolynomial
          f).comp
      (HexPolyFpMathlib.toMathlibPolynomial
        g)

The finite-field transport intertwines executable Horner composition with Mathlib polynomial composition.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_dvd {p : ℕ} [Hex.ZMod64.Bounds p]
  {f g : Hex.FpPoly p} (h : f ∣ g) :
  HexPolyFpMathlib.toMathlibPolynomial f ∣
    HexPolyFpMathlib.toMathlibPolynomial g
HexPolyFpMathlib.toMathlibPolynomial_dvd
  {p : ℕ} [Hex.ZMod64.Bounds p]
  {f g : Hex.FpPoly p} (h : f ∣ g) :
  HexPolyFpMathlib.toMathlibPolynomial f ∣
    HexPolyFpMathlib.toMathlibPolynomial g

Divisibility transports along the finite-field polynomial map.

🔗theorem
HexPolyFpMathlib.toMathlibPolynomial_dvd_iff {p : ℕ}
  [Hex.ZMod64.Bounds p] {f g : Hex.FpPoly p} :
  HexPolyFpMathlib.toMathlibPolynomial f ∣
      HexPolyFpMathlib.toMathlibPolynomial g ↔
    f ∣ g
HexPolyFpMathlib.toMathlibPolynomial_dvd_iff
  {p : ℕ} [Hex.ZMod64.Bounds p]
  {f g : Hex.FpPoly p} :
  HexPolyFpMathlib.toMathlibPolynomial f ∣
      HexPolyFpMathlib.toMathlibPolynomial
        g ↔
    f ∣ g

Executable finite-field polynomials divide one another exactly when their Mathlib images do.

The inverse map also has named rules for the basic constructors and ring operations. In particular, a caller going backward across the equivalence does not need to combine RingEquiv.symm_apply_eq with a forward coefficient proof.

🔗theorem
HexPolyFpMathlib.polynomialToFpPoly_zero {p : ℕ} [Hex.ZMod64.Bounds p] :
  HexPolyFpMathlib.polynomialToFpPoly 0 = 0
HexPolyFpMathlib.polynomialToFpPoly_zero
  {p : ℕ} [Hex.ZMod64.Bounds p] :
  HexPolyFpMathlib.polynomialToFpPoly 0 =
    0

The inverse transport sends Mathlib's zero polynomial to executable zero.

🔗theorem
HexPolyFpMathlib.polynomialToFpPoly_one {p : ℕ} [Hex.ZMod64.Bounds p] :
  HexPolyFpMathlib.polynomialToFpPoly 1 = 1
HexPolyFpMathlib.polynomialToFpPoly_one
  {p : ℕ} [Hex.ZMod64.Bounds p] :
  HexPolyFpMathlib.polynomialToFpPoly 1 =
    1

The inverse transport sends Mathlib's one polynomial to executable one.

🔗theorem
HexPolyFpMathlib.polynomialToFpPoly_C {p : ℕ} [Hex.ZMod64.Bounds p]
  (c : ZMod p) :
  HexPolyFpMathlib.polynomialToFpPoly (Polynomial.C c) =
    Hex.DensePoly.C (HexModArithMathlib.ZMod64.ofZMod c)
HexPolyFpMathlib.polynomialToFpPoly_C
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (c : ZMod p) :
  HexPolyFpMathlib.polynomialToFpPoly
      (Polynomial.C c) =
    Hex.DensePoly.C
      (HexModArithMathlib.ZMod64.ofZMod c)

The inverse transport sends a Mathlib constant to the corresponding executable constant.

🔗theorem
HexPolyFpMathlib.polynomialToFpPoly_neg {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Polynomial (ZMod p)) :
  HexPolyFpMathlib.polynomialToFpPoly (-f) =
    -HexPolyFpMathlib.polynomialToFpPoly f
HexPolyFpMathlib.polynomialToFpPoly_neg
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Polynomial (ZMod p)) :
  HexPolyFpMathlib.polynomialToFpPoly
      (-f) =
    -HexPolyFpMathlib.polynomialToFpPoly f

The inverse transport commutes with polynomial negation.

🔗theorem
HexPolyFpMathlib.polynomialToFpPoly_sub {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Polynomial (ZMod p)) :
  HexPolyFpMathlib.polynomialToFpPoly (f - g) =
    HexPolyFpMathlib.polynomialToFpPoly f -
      HexPolyFpMathlib.polynomialToFpPoly g
HexPolyFpMathlib.polynomialToFpPoly_sub
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Polynomial (ZMod p)) :
  HexPolyFpMathlib.polynomialToFpPoly
      (f - g) =
    HexPolyFpMathlib.polynomialToFpPoly
        f -
      HexPolyFpMathlib.polynomialToFpPoly
        g

The inverse transport commutes with polynomial subtraction.

🔗theorem
HexPolyFpMathlib.polynomialToFpPoly_add {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Polynomial (ZMod p)) :
  HexPolyFpMathlib.polynomialToFpPoly (f + g) =
    HexPolyFpMathlib.polynomialToFpPoly f +
      HexPolyFpMathlib.polynomialToFpPoly g
HexPolyFpMathlib.polynomialToFpPoly_add
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Polynomial (ZMod p)) :
  HexPolyFpMathlib.polynomialToFpPoly
      (f + g) =
    HexPolyFpMathlib.polynomialToFpPoly
        f +
      HexPolyFpMathlib.polynomialToFpPoly
        g

The inverse transport commutes with polynomial addition.

🔗theorem
HexPolyFpMathlib.polynomialToFpPoly_mul {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Polynomial (ZMod p)) :
  HexPolyFpMathlib.polynomialToFpPoly (f * g) =
    HexPolyFpMathlib.polynomialToFpPoly f *
      HexPolyFpMathlib.polynomialToFpPoly g
HexPolyFpMathlib.polynomialToFpPoly_mul
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (f g : Polynomial (ZMod p)) :
  HexPolyFpMathlib.polynomialToFpPoly
      (f * g) =
    HexPolyFpMathlib.polynomialToFpPoly
        f *
      HexPolyFpMathlib.polynomialToFpPoly
        g

The inverse transport commutes with polynomial multiplication.

🔗theorem
HexPolyFpMathlib.polynomialToFpPoly_monomial {p : ℕ}
  [Hex.ZMod64.Bounds p] (n : ℕ) (c : ZMod p) :
  HexPolyFpMathlib.polynomialToFpPoly ((Polynomial.monomial n) c) =
    Hex.DensePoly.monomial n (HexModArithMathlib.ZMod64.ofZMod c)
HexPolyFpMathlib.polynomialToFpPoly_monomial
  {p : ℕ} [Hex.ZMod64.Bounds p] (n : ℕ)
  (c : ZMod p) :
  HexPolyFpMathlib.polynomialToFpPoly
      ((Polynomial.monomial n) c) =
    Hex.DensePoly.monomial n
      (HexModArithMathlib.ZMod64.ofZMod c)

The inverse transport sends a Mathlib monomial to the corresponding executable monomial.

The correspondence layer stops at representation-level facts. A statement mentioning Berlekamp's basis size or Rabin's test does not belong here even when its conclusion is about HexPolyFpMathlib.toMathlibPolynomial: that is a fact about a factoring algorithm rather than about the representation, and it lives in HexBerlekampMathlib.

8.6.3. Mathlib algebraic structure🔗

A RingEquiv does not install a CommRing. Without one, Hex.FpPoly p →+* R is not a well-formed type, so the instance is a prerequisite for every ring homomorphism out of the executable polynomials rather than a convenience.

🔗def
HexPolyFpMathlib.commRing {p : ℕ} [Hex.ZMod64.Bounds p] :
  CommRing (Hex.FpPoly p)
HexPolyFpMathlib.commRing {p : ℕ}
  [Hex.ZMod64.Bounds p] :
  CommRing (Hex.FpPoly p)

The executable prime-field polynomials are a Mathlib commutative ring, with the executable operations. Built from the laws HexPolyFp.Ring proves rather than transported along HexPolyFpMathlib.fpPolyEquiv, which would attach the right laws to Mathlib's operations instead of these.

sub and neg are pinned to the executable ones rather than left at the minimal-axioms defaults (a - b = a + -b). HexPolyFp already defines Sub and Neg, so leaving the defaults would put two different subtractions on the type and Mathlib's lemmas would not fire on the spelling callers write.

The design point is worth restating, because the obvious alternative is the wrong one. Transporting a CommRing along HexPolyFpMathlib.fpPolyEquiv would produce a correct instance whose operations are Mathlib's: f * g would mean "map both sides into Polynomial (ZMod p), multiply there, map back", and none of the executable convolution would run. Building the instance from the laws HexPolyFp proves keeps the operations the executable ones, so multiplication under it is still the schoolbook loop.

open Hex in example {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : f * g = DensePoly.mul f g := rfl

Mathlib's ring automation therefore applies directly to the fast representation:

open Hex in example {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : (f + g) ^ 2 = f ^ 2 + 2 * (f * g) + g ^ 2 := p:ℕinst✝:ZMod64.Bounds pf:FpPoly pg:FpPoly p⊢ (f + g) ^ 2 = f ^ 2 + 2 * (f * g) + g ^ 2 All goals completed! 🐙

One executable operation needs to be identified with its Mathlib counterpart by hand, because HexPolyFp defines it by structural recursion for kernel reduction while the CommRing above supplies npowRec.

🔗theorem
HexPolyFpMathlib.linearPow_eq_pow {p : ℕ} [Hex.ZMod64.Bounds p]
  (b : Hex.FpPoly p) (k : ℕ) : b.linearPow k = b ^ k
HexPolyFpMathlib.linearPow_eq_pow {p : ℕ}
  [Hex.ZMod64.Bounds p] (b : Hex.FpPoly p)
  (k : ℕ) : b.linearPow k = b ^ k

The executable linear power is Mathlib's monoid power. HexPolyFp defines linearPow by structural recursion for kernel reduction; the CommRing above supplies npowRec. They agree, and saying so once lets map_pow be used on executable powers.

Finally, a naming note for readers of older code. The equivalence and its transports lived in HexBerlekampMathlib while Berlekamp factoring was their only consumer, and that library still re-exports the correspondence names, so a call site spelling one of them HexBerlekampMathlib.toMathlibPolynomial keeps resolving.