hex

8.3. Constructors and conversions🔗

The primitive constructor takes any Nat, reduces it modulo p, and packages the result with its reduction proof. An OfNat instance routes numeric literals through it, so (3 : ZMod64 7) denotes the residue of 3.

🔗def
Hex.ZMod64.ofNat (p n : ℕ) [Hex.ZMod64.Bounds p] : Hex.ZMod64 p
Hex.ZMod64.ofNat (p n : ℕ)
  [Hex.ZMod64.Bounds p] : Hex.ZMod64 p

Build a reduced residue by taking the Nat representative mod p.

The bound p ≤ 2^64 ensures the reduced representative is stored faithfully in the backing UInt64.

Its defining property is that the representative of ofNat p n is n reduced modulo p. Every coefficient computation rewrites across this identity.

🔗theorem
Hex.ZMod64.toNat_ofNat {p : ℕ} [Hex.ZMod64.Bounds p] (n : ℕ) :
  (Hex.ZMod64.ofNat p n).toNat = n % p
Hex.ZMod64.toNat_ofNat {p : ℕ}
  [Hex.ZMod64.Bounds p] (n : ℕ) :
  (Hex.ZMod64.ofNat p n).toNat = n % p

The Nat representative of ofNat p n is n reduced modulo p.