theorem HexGFqMathlib.ofPolyHom_reduceMod {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} (y : Hex.FpPoly p) : (ofPolyHom f hf hp hirr) (Hex.GFqRing.reduceMod f y) = (ofPolyHom f hf hp hirr) y

Reduction modulo the modulus is invisible after passing to the field.

theorem HexGFqMathlib.ofPolyHom_modByMonic {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} (hm : Hex.DensePoly.Monic f) (y : Hex.FpPoly p) : (ofPolyHom f hf hp hirr) (f.modByMonic y hm) = (ofPolyHom f hf hp hirr) y

The modByMonic spelling of HexGFqMathlib.ofPolyHom_reduceMod.

theorem HexGFqMathlib.ofPolyHom_linPowMod {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} (hm : Hex.DensePoly.Monic f) (x : Hex.FpPoly p) (k : ℕ) : (ofPolyHom f hf hp hirr) (Hex.Conway.linPowMod f hm x k) = (ofPolyHom f hf hp hirr) x ^ k

The executable structural power carries to a Mathlib power.

This is clean now only because HexGFqMathlib.field pins npow to the executable power: with Mathlib's npowRec default the two would not be definitionally equal and pow_zero/pow_succ would not apply to the ^ that elaboration picks here.

theorem HexGFqMathlib.ofPolyHom_powerResidue {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} (hm : Hex.DensePoly.Monic f) (k : ℕ) : (ofPolyHom f hf hp hirr) (Hex.Conway.powerResidue f hm k) = (ofPolyHom f hf hp hirr) Hex.FpPoly.X ^ k

The binary generator power represents the corresponding field power.

theorem HexGFqMathlib.reduceMod_powerResidue {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} (hm : Hex.DensePoly.Monic f) (k : ℕ) : Hex.GFqRing.reduceMod f (Hex.Conway.powerResidue f hm k) = Hex.Conway.powerResidue f hm k

A generator power representative is already reduced.

theorem HexGFqMathlib.ofPolyHom_eq_one_iff {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} {y : Hex.FpPoly p} (hy : Hex.GFqRing.reduceMod f y = y) : (ofPolyHom f hf hp hirr) y = 1 ↔ y = 1

On reduced representatives, being one in the field is being one on the nose.

theorem HexGFqMathlib.mathlibPrime_of_hexPrime {q : ℕ} (h : Hex.Nat.Prime q) : Nat.Prime q

Hex's Mathlib-free prime predicate implies Mathlib's.

theorem HexGFqMathlib.mem_of_prime_dvd_primePowerProduct (qs es : List ℕ) {q : ℕ} : Nat.Prime q → (∀ r ∈ qs, Nat.Prime r) → q ∣ Hex.Conway.primePowerProduct qs es → q ∈ qs

Every prime dividing a validated prime-power product appears in its prime list. This is unique factorization in the form the check needs: it is what turns "the supplied primes multiply to N" into "the supplied primes are all of them", so a short list cannot weaken the test.

theorem HexGFqMathlib.orderOf_gen_of_primitive {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {n : ℕ} (h : Hex.Conway.SupportedEntry p n) {qs es : List ℕ} (hprimitive : Hex.Conway.Primitive p n h qs es) : orderOf (Hex.GFq.ofPoly h Hex.FpPoly.X) = p ^ n - 1

A verified executable primitivity certificate proves that the Conway generator has multiplicative order p ^ n - 1.

This is the assembly point for the component transport lemmas above. The factorization check makes qs exhaustive, while the two power checks become the hypotheses of orderOf_eq_of_pow_and_pow_div_prime.