15.4. Key correctness theorems🔗

The proof obligations that promote the wrapper from a ring to a field are the inverse-cancellation laws. For any nonzero element, the extended-GCD inverse is a genuine two-sided multiplicative inverse.

theorem

Hex.GFqField.mul_inv_cancel {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} {x : Hex.GFqField.FiniteField f hf hp hirr}
  (hx : x ≠ 0) : x * x⁻¹ = 1
Hex.GFqField.mul_inv_cancel {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  {x :
    Hex.GFqField.FiniteField f hf hp hirr}
  (hx : x ≠ 0) : x * x⁻¹ = 1

A nonzero field element cancels against its inverse on the right.

theorem

Hex.GFqField.inv_mul_cancel {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} {x : Hex.GFqField.FiniteField f hf hp hirr}
  (hx : x ≠ 0) : x⁻¹ * x = 1
Hex.GFqField.inv_mul_cancel {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  {x :
    Hex.GFqField.FiniteField f hf hp hirr}
  (hx : x ≠ 0) : x⁻¹ * x = 1

A nonzero field element cancels against its inverse on the left.

Division is definitionally multiplication by the inverse, and the field is nontrivial (0 ≠ 1), which is where irreducibility (hence a positive-degree modulus) is used.

theorem

Hex.GFqField.div_eq_mul_inv {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} (x y : Hex.GFqField.FiniteField f hf hp hirr) :
  x / y = x * y⁻¹
Hex.GFqField.div_eq_mul_inv {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x y :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  x / y = x * y⁻¹

Division is field multiplication by inverse.

theorem

Hex.GFqField.zero_ne_one {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (hf : 0 < f.degree) (hp : Hex.Nat.Prime p)
  (hirr : f.Irreducible) : 0 ≠ 1
Hex.GFqField.zero_ne_one {p : Nat}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hf : 0 < f.degree)
  (hp : Hex.Nat.Prime p)
  (hirr : f.Irreducible) : 0 ≠ 1

The quotient-field wrapper is nontrivial.

The Frobenius endomorphism is definitionally the p-th power map, the form downstream code uses.

theorem

Hex.GFqField.frob_eq_pow {p : Nat} [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p} {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible} (x : Hex.GFqField.FiniteField f hf hp hirr) :
  Hex.GFqField.frob x = x ^ p
Hex.GFqField.frob_eq_pow {p : Nat}
  [Hex.ZMod64.Bounds p]
  {hp : Hex.Nat.Prime p}
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  {hirr : f.Irreducible}
  (x :
    Hex.GFqField.FiniteField f hf hp
      hirr) :
  Hex.GFqField.frob x = x ^ p

Frobenius is definitionally the p-th power map.

These laws, together with the ring axioms inherited from HexGFqRing, are bundled into a Lean.Grind.Field instance on Hex.GFqField.FiniteField, plus a Lean.Grind.IsCharP instance recording characteristic p. That instance is the entry point for downstream proof automation over the executable finite field.