class Hex.ZMod64.PrimeModulus (p : Nat) : Prop

Typeclass wrapper for the prime-modulus assumption needed by field-style facts over ZMod64 p.

• prime : Nat.Prime p

theorem Hex.ZMod64.primeModulusOfPrime {p : Nat} (hp : Nat.Prime p) : PrimeModulus p

Build the prime-modulus typeclass witness from an explicit project-local primality proof.

theorem Hex.ZMod64.one_ne_zero_of_prime {p : Nat} [Bounds p] (hp : Nat.Prime p) : 1 ≠ 0

1 ≠ 0 in ZMod64 p when p is prime.

theorem Hex.ZMod64.one_ne_zero {p : Nat} [Bounds p] [PrimeModulus p] : 1 ≠ 0

Typeclass form of one_ne_zero_of_prime.

theorem Hex.ZMod64.eq_zero_or_eq_zero_of_mul_eq_zero {p : Nat} [Bounds p] (hp : Nat.Prime p) {a b : ZMod64 p} (h : a * b = 0) : a = 0 ∨ b = 0

Prime-modulus residues have no zero divisors: if a * b = 0, then one of the factors is already zero.

theorem Hex.ZMod64.eq_zero_or_eq_zero_of_mul_eq_zero_of_prime_modulus {p : Nat} [Bounds p] [PrimeModulus p] {a b : ZMod64 p} (h : a * b = 0) : a = 0 ∨ b = 0

Prime-modulus residues have no zero divisors, using the ambient PrimeModulus typeclass witness.

theorem Hex.ZMod64.inv_mul_eq_one_of_prime {p : Nat} [Bounds p] (hp : Nat.Prime p) {a : ZMod64 p} (ha : a ≠ 0) : a.inv * a = 1

Nonzero residues modulo a prime have multiplicative inverses.

theorem Hex.ZMod64.inv_mul_eq_one_of_ne_zero {p : Nat} [Bounds p] [PrimeModulus p] {a : ZMod64 p} (ha : a ≠ 0) : a.inv * a = 1

Nonzero residues modulo an ambient prime modulus have multiplicative inverses.

theorem Hex.ZMod64.mul_inv_eq_one_of_prime {p : Nat} [Bounds p] (hp : Nat.Prime p) {a : ZMod64 p} (ha : a ≠ 0) : a * a.inv = 1

Symmetric form of inv_mul_eq_one_of_prime: a * a⁻¹ = 1.

theorem Hex.ZMod64.mul_inv_eq_one_of_ne_zero {p : Nat} [Bounds p] [PrimeModulus p] {a : ZMod64 p} (ha : a ≠ 0) : a * a.inv = 1

Symmetric form of inv_mul_eq_one_of_ne_zero: a * a⁻¹ = 1.

theorem Hex.ZMod64.pow_prime {p : Nat} [Bounds p] (hp : Nat.Prime p) (a : ZMod64 p) : a ^ p = a

Fermat's little theorem for Hex.ZMod64: raising a residue mod a prime p to the pth power returns the original residue.

@[simp]

theorem Hex.ZMod64.pow_prime_of_prime_modulus {p : Nat} [Bounds p] [PrimeModulus p] (a : ZMod64 p) : a ^ p = a

Fermat's little theorem for an ambient prime modulus.