instance HexModArithMathlib.ZMod64.instNeZeroNat_hexModArithMathlib {p : ℕ} [Hex.ZMod64.Bounds p] : NeZero p

def 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.

Equations

• HexModArithMathlib.ZMod64.toZMod a = ↑a.toNat

def 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.

Equations

• HexModArithMathlib.ZMod64.ofZMod a = Hex.ZMod64.ofNat p a.val

@[simp]

theorem HexModArithMathlib.ZMod64.val_toZMod {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p) : (toZMod a).val = a.toNat

The canonical representative of a transferred class is the executable residue's Nat value: (toZMod a).val = a.toNat. Callers reading the Mathlib-side val of a transferred element recover the machine residue without unfolding the conversion.

@[simp]

theorem HexModArithMathlib.ZMod64.ofZMod_toZMod {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p) : ofZMod (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.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_ofZMod {p : ℕ} [Hex.ZMod64.Bounds p] (a : ZMod p) : toZMod (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.

@[simp]

theorem HexModArithMathlib.ZMod64.ofZMod_zero {p : ℕ} [Hex.ZMod64.Bounds p] : ofZMod 0 = 0

ofZMod carries Mathlib's 0 to the executable 0, so transferring the additive identity in from ZMod lands on ZMod64's identity.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_zero {p : ℕ} [Hex.ZMod64.Bounds p] : toZMod 0 = 0

toZMod carries the executable 0 to Mathlib's 0, so the additive identity transfers out to ZMod's identity.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_one {p : ℕ} [Hex.ZMod64.Bounds p] : toZMod 1 = 1

toZMod carries the executable 1 to Mathlib's 1, so the multiplicative identity transfers out to ZMod's identity.

@[simp]

theorem HexModArithMathlib.ZMod64.ofZMod_one {p : ℕ} [Hex.ZMod64.Bounds p] : ofZMod 1 = 1

ofZMod carries Mathlib's 1 to the executable 1, so the multiplicative identity transfers in from ZMod to ZMod64.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_add {p : ℕ} [Hex.ZMod64.Bounds p] (a b : Hex.ZMod64 p) : toZMod (a + b) = toZMod a + 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.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_neg {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p) : toZMod (-a) = -toZMod a

toZMod commutes with negation, so additive inverses transfer out to ZMod.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_sub {p : ℕ} [Hex.ZMod64.Bounds p] (a b : Hex.ZMod64 p) : toZMod (a - b) = toZMod a - toZMod b

toZMod commutes with subtraction, so differences transfer out to ZMod.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_mul {p : ℕ} [Hex.ZMod64.Bounds p] (a b : Hex.ZMod64 p) : toZMod (a * b) = toZMod a * 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.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_natCast {p : ℕ} [Hex.ZMod64.Bounds p] (n : ℕ) : toZMod ↑n = ↑n

toZMod commutes with the Nat cast: a numeral built in ZMod64 transfers to the same numeral in ZMod. Lets callers move Nat-literal coefficients across the correspondence.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_intCast {p : ℕ} [Hex.ZMod64.Bounds p] (z : ℤ) : toZMod ↑z = ↑z

toZMod commutes with the Int cast: an integer built in ZMod64 transfers to the same integer in ZMod. Lets callers move signed integer coefficients across the correspondence.

@[simp]

theorem HexModArithMathlib.ZMod64.toZMod_pow {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p) (n : ℕ) : toZMod (a ^ n) = toZMod a ^ n

toZMod commutes with Nat powers, so exponentiation transfers out to ZMod.

def 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.

Equations

• HexModArithMathlib.ZMod64.equiv = { toFun := HexModArithMathlib.ZMod64.toZMod, invFun := HexModArithMathlib.ZMod64.ofZMod, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem HexModArithMathlib.ZMod64.equiv_apply {p : ℕ} [Hex.ZMod64.Bounds p] (a : Hex.ZMod64 p) : equiv a = toZMod a

equiv acts as toZMod on elements. Rewrites the bundled ring equivalence to the bare conversion, so the transport @[simp] lemmas above fire on equiv applications.

@[simp]

theorem HexModArithMathlib.ZMod64.equiv_symm_apply {p : ℕ} [Hex.ZMod64.Bounds p] (a : ZMod p) : equiv.symm a = ofZMod a

equiv.symm acts as ofZMod on elements. Rewrites the inverse ring equivalence to the bare conversion, so the transport @[simp] lemmas above fire on equiv.symm applications.