@[instance_reducible]

instance Hex.ZMod64.instDiv {p : Nat} [Bounds p] : Div (ZMod64 p)

Equations

• Hex.ZMod64.instDiv = { div := fun (a b : Hex.ZMod64 p) => a.mul b.inv }

def Hex.ZMod64.intPow {p : Nat} [Bounds p] (a : ZMod64 p) : Int → ZMod64 p

Integer powers in the prime field, using inverses for negative exponents.

Equations

• a.intPow (Int.ofNat n) = a ^ n
• a.intPow (Int.negSucc n) = (a ^ (n + 1))⁻¹

theorem Hex.ZMod64.inv_zero_of_zero {p : Nat} [Bounds p] : 0⁻¹ = 0

The 0⁻¹ = 0 junk-value convention for ZMod64 p.

theorem Hex.ZMod64.inv_ne_zero_of_prime {p : Nat} [Bounds p] (hp : Nat.Prime p) {a : ZMod64 p} (ha : a ≠ 0) : a⁻¹ ≠ 0

The inverse of a nonzero residue modulo a prime is itself nonzero.

theorem Hex.ZMod64.inv_inv_of_prime {p : Nat} [Bounds p] (hp : Nat.Prime p) (a : ZMod64 p) : a⁻¹⁻¹ = a

Double-inverse identity in ZMod64 p for a prime modulus.

@[instance_reducible]

instance Hex.zmod64FieldOfPrime {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : Lean.Grind.Field (ZMod64 p)

The Lean.Grind.Field instance on Hex.ZMod64 p carried by a prime-modulus witness.

Equations

• One or more equations did not get rendered due to their size.