4.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 Hex.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 Hex.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 Hex.ZMod64 → ZMod → Hex.ZMod64 is the identity. This is the left-inverse law making HexModArithMathlib.ZMod64.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 → Hex.ZMod64 → ZMod is the identity. Together with HexModArithMathlib.ZMod64.ofZMod_toZMod, this shows the two conversions are mutually inverse and define a ring equivalence.

HexModArithMathlib.ZMod64.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

HexModArithMathlib.ZMod64.toZMod is additive, so callers can push the conversion through a sum and transfer additive ZMod identities back to Hex.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

HexModArithMathlib.ZMod64.toZMod is multiplicative, so callers can push the conversion through a product and transfer multiplicative ZMod identities back to Hex.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 Hex.ZMod64 representation is ring-equivalent to Mathlib's ZMod.