8.7. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexModArithMathlib connects it to Mathlib: every Hex.ZMod64 value corresponds to an element of Mathlib's ZMod p. The two transfer maps convert a residue to a ZMod p element and back.

def

HexModArithMathlib.ZMod64.toZMod {p : ℕ} [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p) : ZMod p
HexModArithMathlib.ZMod64.toZMod {p : ℕ}
  [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p) : ZMod p

Interpret an executable ZMod64 residue as a Mathlib ZMod class.

def

HexModArithMathlib.ZMod64.ofZMod {p : ℕ} [Hex.ZMod64.Bounds p]
  (a : ZMod p) : Hex.ZMod64 p
HexModArithMathlib.ZMod64.ofZMod {p : ℕ}
  [Hex.ZMod64.Bounds p] (a : ZMod p) :
  Hex.ZMod64 p

Rebuild an executable ZMod64 residue from a Mathlib ZMod class.

They are mutually inverse:

theorem

HexModArithMathlib.ZMod64.ofZMod_toZMod {p : ℕ} [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p) :
  HexModArithMathlib.ZMod64.ofZMod
      (HexModArithMathlib.ZMod64.toZMod a) =
    a
HexModArithMathlib.ZMod64.ofZMod_toZMod
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (a : Hex.ZMod64 p) :
  HexModArithMathlib.ZMod64.ofZMod
      (HexModArithMathlib.ZMod64.toZMod
        a) =
    a

Round-trip ZMod64 → ZMod → ZMod64 is the identity. This is the left-inverse law making toZMod injective; a caller that transfers a residue to Mathlib and back recovers it unchanged.

theorem

HexModArithMathlib.ZMod64.toZMod_ofZMod {p : ℕ} [Hex.ZMod64.Bounds p]
  (a : ZMod p) :
  HexModArithMathlib.ZMod64.toZMod
      (HexModArithMathlib.ZMod64.ofZMod a) =
    a
HexModArithMathlib.ZMod64.toZMod_ofZMod
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (a : ZMod p) :
  HexModArithMathlib.ZMod64.toZMod
      (HexModArithMathlib.ZMod64.ofZMod
        a) =
    a

Round-trip ZMod → ZMod64 → ZMod is the identity. Together with ofZMod_toZMod this shows the two conversions are mutually inverse, so equiv below is a genuine ring equivalence.

toZMod preserves the ring operations: addition and multiplication transfer, as do negation, subtraction, the casts, and powers (each a @[simp] lemma):

theorem

HexModArithMathlib.ZMod64.toZMod_add {p : ℕ} [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) :
  HexModArithMathlib.ZMod64.toZMod (a + b) =
    HexModArithMathlib.ZMod64.toZMod a +
      HexModArithMathlib.ZMod64.toZMod b
HexModArithMathlib.ZMod64.toZMod_add
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) :
  HexModArithMathlib.ZMod64.toZMod
      (a + b) =
    HexModArithMathlib.ZMod64.toZMod a +
      HexModArithMathlib.ZMod64.toZMod b

toZMod is additive. This is the additive-homomorphism law underlying equiv; it lets a caller push toZMod through a sum and so transfer any additive ZMod identity back to ZMod64.

theorem

HexModArithMathlib.ZMod64.toZMod_mul {p : ℕ} [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) :
  HexModArithMathlib.ZMod64.toZMod (a * b) =
    HexModArithMathlib.ZMod64.toZMod a *
      HexModArithMathlib.ZMod64.toZMod b
HexModArithMathlib.ZMod64.toZMod_mul
  {p : ℕ} [Hex.ZMod64.Bounds p]
  (a b : Hex.ZMod64 p) :
  HexModArithMathlib.ZMod64.toZMod
      (a * b) =
    HexModArithMathlib.ZMod64.toZMod a *
      HexModArithMathlib.ZMod64.toZMod b

toZMod is multiplicative. This is the multiplicative-homomorphism law underlying equiv; it lets a caller push toZMod through a product and so transfer any multiplicative ZMod identity back to ZMod64.

The maps and laws bundle into a ring equivalence, so the CommRing theory of ZMod p transports to the executable type:

def

HexModArithMathlib.ZMod64.equiv {p : ℕ} [Hex.ZMod64.Bounds p] :
  Hex.ZMod64 p ≃+* ZMod p
HexModArithMathlib.ZMod64.equiv {p : ℕ}
  [Hex.ZMod64.Bounds p] :
  Hex.ZMod64 p ≃+* ZMod p

The executable ZMod64 representation is ring-equivalent to Mathlib's ZMod.