Documentation

HexModArith.Ring

def Hex.ZMod64.neg {p : Nat} [Bounds p] (a : ZMod64 p) :

The additive inverse represented by the complementary residue mod p.

Equations

a.neg = if hzero : a.val = 0 then { val := 0, isLt := ⋯ } else { val := -a.val - Hex.ZMod64.complementWord p ⋯, isLt := ⋯ }

Instances For

def Hex.ZMod64.natCast (p : Nat) [Bounds p] (n : Nat) :

Natural-number literals in ZMod64.

Equations

Hex.ZMod64.natCast p n = Hex.ZMod64.ofNat p n

Instances For

def Hex.ZMod64.nsmul {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) :

Natural scalar multiplication on ZMod64.

Equations

Hex.ZMod64.nsmul n a = Hex.ZMod64.ofNat p (n * a.toNat)

Instances For

def Hex.ZMod64.intCast (p : Nat) [Bounds p] :

Int → ZMod64 p

Integer literals in ZMod64, reduced mod p.

Equations

Hex.ZMod64.intCast p (Int.ofNat n) = Hex.ZMod64.natCast p n
Hex.ZMod64.intCast p (Int.negSucc n) = (Hex.ZMod64.natCast p (n + 1)).neg

Instances For

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

Integer scalar multiplication on ZMod64.

Equations

Hex.ZMod64.zsmul (Int.ofNat n) a = Hex.ZMod64.nsmul n a
Hex.ZMod64.zsmul (Int.negSucc n) a = (Hex.ZMod64.nsmul (n + 1) a).neg

Instances For

@[simp]

theorem Hex.ZMod64.intCast_ofNat {p : Nat} [Bounds p] (n : Nat) :

intCast p (Int.ofNat n) = natCast p n

Integer casts of nonnegative representatives agree with natural casts.

@[simp]

theorem Hex.ZMod64.intCast_negSucc {p : Nat} [Bounds p] (n : Nat) :

intCast p (Int.negSucc n) = (natCast p (n + 1)).neg

Integer casts of negative representatives use the complementary natural cast.

@[simp]

theorem Hex.ZMod64.zsmul_ofNat {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) :

zsmul (Int.ofNat n) a = nsmul n a

Integer scalar multiplication by a nonnegative integer is natural scalar multiplication.

@[simp]

theorem Hex.ZMod64.zsmul_negSucc {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) :

zsmul (Int.negSucc n) a = (nsmul (n + 1) a).neg

Integer scalar multiplication by a negative integer negates the positive natural multiple.

@[instance_reducible]

instance Hex.ZMod64.instNeg {p : Nat} [Bounds p] :

Equations

Hex.ZMod64.instNeg = { neg := Hex.ZMod64.neg }

@[instance_reducible]

instance Hex.ZMod64.instNatCast {p : Nat} [Bounds p] :

NatCast (ZMod64 p)

Equations

Hex.ZMod64.instNatCast = { natCast := Hex.ZMod64.natCast p }

@[instance_reducible]

instance Hex.ZMod64.instOfNat {p : Nat} [Bounds p] (n : Nat) :

OfNat (ZMod64 p) n

Equations

Hex.ZMod64.instOfNat n = { ofNat := Hex.ZMod64.natCast p n }

@[instance_reducible]

instance Hex.ZMod64.instSMulNat {p : Nat} [Bounds p] :

SMul Nat (ZMod64 p)

Equations

Hex.ZMod64.instSMulNat = { smul := Hex.ZMod64.nsmul }

@[instance_reducible]

instance Hex.ZMod64.instIntCast {p : Nat} [Bounds p] :

IntCast (ZMod64 p)

Equations

Hex.ZMod64.instIntCast = { intCast := Hex.ZMod64.intCast p }

@[instance_reducible]

instance Hex.ZMod64.instSMulInt {p : Nat} [Bounds p] :

SMul Int (ZMod64 p)

Equations

Hex.ZMod64.instSMulInt = { smul := Hex.ZMod64.zsmul }

@[simp]

theorem Hex.ZMod64.toNat_natCast {p : Nat} [Bounds p] (n : Nat) :

(natCast p n).toNat = n % p

Natural casts reduce their representative modulo p.

theorem Hex.ZMod64.natCast_eq_ofNat {p : Nat} [Bounds p] (n : Nat) :

natCast p n = ofNat p n

Natural casts are residues built from the cast representative.

theorem Hex.ZMod64.natCast_op_eq_ofNat {p : Nat} [Bounds p] (n : Nat) :

↑n = ofNat p n

Operator-level form of natCast_eq_ofNat.

@[simp]

theorem Hex.ZMod64.toNat_neg {p : Nat} [Bounds p] (a : ZMod64 p) :

a.neg.toNat = (p - a.toNat) % p

Negation takes the complementary representative modulo p.

theorem Hex.ZMod64.neg_eq_ofNat {p : Nat} [Bounds p] (a : ZMod64 p) :

a.neg = ofNat p (p - a.toNat)

Negation is the residue built from the complementary representative.

theorem Hex.ZMod64.neg_op_eq_ofNat {p : Nat} [Bounds p] (a : ZMod64 p) :

-a = ofNat p (p - a.toNat)

Operator-level form of neg_eq_ofNat.

@[simp]

theorem Hex.ZMod64.toNat_nsmul {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) :

(nsmul n a).toNat = n * a.toNat % p

Natural scalar multiplication reduces the scaled representative modulo p.

theorem Hex.ZMod64.nsmul_eq_ofNat {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) :

nsmul n a = ofNat p (n * a.toNat)

Natural scalar multiplication is the residue built from the scaled representative.

theorem Hex.ZMod64.nsmul_op_eq_ofNat {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) :

n • a = ofNat p (n * a.toNat)

Operator-level form of nsmul_eq_ofNat.

@[simp]

theorem Hex.ZMod64.toNat_intCast_ofNat {p : Nat} [Bounds p] (n : Nat) :

(intCast p (Int.ofNat n)).toNat = n % p

Integer casts of nonnegative representatives reduce modulo p.

@[simp]

theorem Hex.ZMod64.toNat_intCast_negSucc {p : Nat} [Bounds p] (n : Nat) :

(intCast p (Int.negSucc n)).toNat = (p - (n + 1) % p) % p

Integer casts of negative representatives use the complementary reduced representative.

@[simp]

theorem Hex.ZMod64.toNat_zsmul_ofNat {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) :

(zsmul (Int.ofNat n) a).toNat = n * a.toNat % p

Nonnegative integer scalar multiplication reduces the scaled representative modulo p.

@[simp]

theorem Hex.ZMod64.toNat_zsmul_negSucc {p : Nat} [Bounds p] (n : Nat) (a : ZMod64 p) :

(zsmul (Int.negSucc n) a).toNat = (p - (n + 1) * a.toNat % p) % p

Negative integer scalar multiplication uses the complementary scaled representative.

theorem Hex.ZMod64.natCast_eq_natCast_iff {p : Nat} [Bounds p] (x y : Nat) :

↑x = ↑y ↔ x % p = y % p

Nat casts agree exactly when their representatives are congruent mod p.

theorem Hex.ZMod64.natCast_eq_zero_iff_dvd {p : Nat} [Bounds p] (n : Nat) :

↑n = 0 ↔ p ∣ n

A Nat literal vanishes in ZMod64 p exactly when p divides it.

@[simp]

theorem Hex.ZMod64.natCast_self {p : Nat} [Bounds p] :

↑p = 0

The modulus itself casts to zero in ZMod64 p.

theorem Hex.ZMod64.toNat_inv {p : Nat} [Bounds p] (a : ZMod64 p) (hcop : a.val.toNat.Coprime p) :

(a.inv * a).toNat = 1 % p

The reference inverse law on canonical representatives.

theorem Hex.ZMod64.nat_add_assoc_mod (x y z m : Nat) :

((x % m + y % m) % m + z % m) % m = (x % m + (y % m + z % m) % m) % m

Associativity of Nat addition under an outer % m, written in the fully reduced form where each operand is already taken % m. This is the reduced-arithmetic identity discharging the additive-associativity ring law on ZMod64 p after the operands are normalised.

theorem Hex.ZMod64.nat_mul_assoc_mod (x y z m : Nat) :

x % m * (y % m) % m * (z % m) % m = x % m * (y % m * (z % m) % m) % m

Associativity of Nat multiplication under an outer % m, with each operand pre-reduced % m. This is the reduced-arithmetic identity discharging the multiplicative-associativity ring law on ZMod64 p.

theorem Hex.ZMod64.nat_left_distrib_mod (x y z m : Nat) :

x % m * ((y % m + z % m) % m) % m = (x % m * (y % m) % m + x % m * (z % m) % m) % m

Left distributivity of Nat multiplication over addition under an outer % m, with each operand pre-reduced % m. This is the reduced-arithmetic identity discharging the left-distributivity ring law on ZMod64 p.

theorem Hex.ZMod64.nat_right_distrib_mod (x y z m : Nat) :

(x % m + y % m) % m * (z % m) % m = (x % m * (z % m) % m + y % m * (z % m) % m) % m

Right distributivity of Nat multiplication over addition under an outer % m, with each operand pre-reduced % m. This is the reduced-arithmetic identity discharging the right-distributivity ring law on ZMod64 p.

theorem Hex.ZMod64.nat_mul_comm_mod (x y m : Nat) :

x * y % m = y * x % m

Commutativity of Nat multiplication under an outer % m. This is the reduced-arithmetic identity discharging the multiplicative-commutativity law of the CommRing (ZMod64 p) instance.

@[instance_reducible]

instance Hex.ZMod64.instSemiring {p : Nat} [Bounds p] :

Lean.Grind.Semiring (ZMod64 p)

Equations

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

@[simp]

theorem Hex.ZMod64.add_zero {p : Nat} [Bounds p] (a : ZMod64 p) :

a + 0 = a

Adding zero on the right leaves a residue unchanged.

@[simp]

theorem Hex.ZMod64.zero_add {p : Nat} [Bounds p] (a : ZMod64 p) :

0 + a = a

Adding zero on the left leaves a residue unchanged.

@[simp]

theorem Hex.ZMod64.mul_zero {p : Nat} [Bounds p] (a : ZMod64 p) :

a * 0 = 0

Multiplying by zero on the right gives zero.

@[simp]

theorem Hex.ZMod64.zero_mul {p : Nat} [Bounds p] (a : ZMod64 p) :

0 * a = 0

Multiplying by zero on the left gives zero.

@[simp]

theorem Hex.ZMod64.mul_one {p : Nat} [Bounds p] (a : ZMod64 p) :

a * 1 = a

Multiplying by one on the right leaves a residue unchanged.

@[simp]

theorem Hex.ZMod64.one_mul {p : Nat} [Bounds p] (a : ZMod64 p) :

1 * a = a

Multiplying by one on the left leaves a residue unchanged.

@[simp]

theorem Hex.ZMod64.pow_zero {p : Nat} [Bounds p] (a : ZMod64 p) :

a ^ 0 = 1

Every residue to the zeroth power is one.

@[simp]

theorem Hex.ZMod64.pow_one {p : Nat} [Bounds p] (a : ZMod64 p) :

a ^ 1 = a

Every residue to the first power is itself.

@[simp]

theorem Hex.ZMod64.pow_succ {p : Nat} [Bounds p] (a : ZMod64 p) (n : Nat) :

a ^ (n + 1) = a ^ n * a

Successor powers multiply the previous power by the base.

@[simp]

theorem Hex.ZMod64.zero_pow {p : Nat} [Bounds p] {n : Nat} (hn : n ≠ 0) :

0 ^ n = 0

Any positive power of zero is zero.

@[simp]

theorem Hex.ZMod64.one_pow {p : Nat} [Bounds p] (n : Nat) :

1 ^ n = 1

Every power of one is one.

@[instance_reducible]

instance Hex.ZMod64.instRing {p : Nat} [Bounds p] :

Lean.Grind.Ring (ZMod64 p)

Equations

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

@[instance_reducible]

instance Hex.ZMod64.instCommRing {p : Nat} [Bounds p] :

Lean.Grind.CommRing (ZMod64 p)

Equations

Hex.ZMod64.instCommRing = { toRing := Hex.ZMod64.instRing, mul_comm := ⋯ }

instance Hex.ZMod64.instIsCharP {p : Nat} [Bounds p] :

Lean.Grind.IsCharP (ZMod64 p) p