theorem HexModArithTheory.ZMod64.toZMod_nsmul {p : ℕ} [Hex.ZMod64.Bounds p] (n : ℕ) (a : Hex.ZMod64 p) : toZMod (n • a) = n • toZMod a

Scalar multiplication by naturals transfers to ZMod.

theorem HexModArithTheory.ZMod64.toZMod_zsmul {p : ℕ} [Hex.ZMod64.Bounds p] (n : ℤ) (a : Hex.ZMod64 p) : toZMod (n • a) = n • toZMod a

Scalar multiplication by integers transfers to ZMod.

@[instance_reducible]

def HexModArithTheory.ZMod64.commRing {p : ℕ} [Hex.ZMod64.Bounds p] : CommRing (Hex.ZMod64 p)

Mathlib's ring laws transported through equiv, retaining every executable operation, including scalar multiplication, casts, subtraction, and powers. Scoped to preserve existing exact Grind instance identities on import.

Equations

• HexModArithTheory.ZMod64.commRing = Function.Injective.commRing HexModArithTheory.ZMod64.toZMod ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯