def Hex.GFqRing.zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) : PolyQuotient f hf

The quotient zero element.

Equations

• Hex.GFqRing.zero f hf = Hex.GFqRing.ofPoly f hf 0

def Hex.GFqRing.one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) : PolyQuotient f hf

The quotient one element.

Equations

• Hex.GFqRing.one f hf = Hex.GFqRing.ofPoly f hf 1

def Hex.GFqRing.const {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (c : ZMod64 p) : PolyQuotient f hf

Embed a prime-field constant as a quotient-ring constant polynomial.

Equations

• Hex.GFqRing.const f hf c = Hex.GFqRing.ofPoly f hf (Hex.FpPoly.C c)

def Hex.GFqRing.add {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : PolyQuotient f hf

Quotient addition reduces the sum of representatives.

Equations

• Hex.GFqRing.add x y = Hex.GFqRing.ofPoly f hf (Hex.GFqRing.repr x + Hex.GFqRing.repr y)

def Hex.GFqRing.mul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : PolyQuotient f hf

Quotient multiplication reduces the product of representatives.

Equations

• Hex.GFqRing.mul x y = Hex.GFqRing.ofPoly f hf ((Hex.GFqRing.repr x).mulPackedFast (Hex.GFqRing.repr y))

def Hex.GFqRing.neg {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : PolyQuotient f hf

Quotient negation reduces the coefficientwise additive inverse.

Equations

• Hex.GFqRing.neg x = Hex.GFqRing.ofPoly f hf (-Hex.GFqRing.repr x)

def Hex.GFqRing.sub {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : PolyQuotient f hf

Quotient subtraction reduces the difference of representatives.

Equations

• Hex.GFqRing.sub x y = Hex.GFqRing.ofPoly f hf (Hex.GFqRing.repr x - Hex.GFqRing.repr y)

def Hex.GFqRing.pow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) (n : Nat) : PolyQuotient f hf

Quotient exponentiation by square-and-multiply on the exponent bits, costing O(log n) quotient-ring multiplications.

Equations

• Hex.GFqRing.pow x n = Hex.GFqRing.pow.go (Hex.GFqRing.one f hf) x n

@[irreducible]

def Hex.GFqRing.pow.go {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (acc base : PolyQuotient f hf) (k : Nat) : PolyQuotient f hf

Equations

• Hex.GFqRing.pow.go acc base k = if hk : k = 0 then acc else have acc' := if k % 2 = 1 then Hex.GFqRing.mul acc base else acc; Hex.GFqRing.pow.go acc' (Hex.GFqRing.mul base base) (k / 2)

def Hex.GFqRing.natCast {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (n : Nat) : PolyQuotient f hf

Natural-number literals in the quotient ring are reduced constant polynomials.

Equations

• Hex.GFqRing.natCast f hf n = Hex.GFqRing.const f hf ↑n

def Hex.GFqRing.nsmul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) (x : PolyQuotient f hf) : PolyQuotient f hf

Natural scalar multiplication in the quotient ring.

Equations

• Hex.GFqRing.nsmul n x = Hex.GFqRing.nsmul.go (Hex.GFqRing.zero f hf) x n

@[irreducible]

def Hex.GFqRing.nsmul.go {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (acc base : PolyQuotient f hf) (k : Nat) : PolyQuotient f hf

Equations

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

def Hex.GFqRing.intCast {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) : Int → PolyQuotient f hf

Integer literals in the quotient ring.

Equations

• Hex.GFqRing.intCast f hf (Int.ofNat n) = Hex.GFqRing.natCast f hf n
• Hex.GFqRing.intCast f hf (Int.negSucc n) = Hex.GFqRing.neg (Hex.GFqRing.natCast f hf (n + 1))

def Hex.GFqRing.zsmul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (i : Int) (x : PolyQuotient f hf) : PolyQuotient f hf

Integer scalar multiplication in the quotient ring.

Equations

• Hex.GFqRing.zsmul (Int.ofNat n) x = Hex.GFqRing.nsmul n x
• Hex.GFqRing.zsmul (Int.negSucc n) x = Hex.GFqRing.neg (Hex.GFqRing.nsmul (n + 1) x)

@[instance_reducible]

instance Hex.GFqRing.instZeroPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Zero (PolyQuotient f hf)

Equations

• Hex.GFqRing.instZeroPolyQuotient = { zero := Hex.GFqRing.zero f hf }

@[instance_reducible]

instance Hex.GFqRing.instOnePolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : One (PolyQuotient f hf)

Equations

• Hex.GFqRing.instOnePolyQuotient = { one := Hex.GFqRing.one f hf }

@[instance_reducible]

instance Hex.GFqRing.instAddPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Add (PolyQuotient f hf)

Equations

• Hex.GFqRing.instAddPolyQuotient = { add := Hex.GFqRing.add }

@[instance_reducible]

instance Hex.GFqRing.instMulPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Mul (PolyQuotient f hf)

Equations

• Hex.GFqRing.instMulPolyQuotient = { mul := Hex.GFqRing.mul }

@[instance_reducible]

instance Hex.GFqRing.instNegPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Neg (PolyQuotient f hf)

Equations

• Hex.GFqRing.instNegPolyQuotient = { neg := Hex.GFqRing.neg }

@[instance_reducible]

instance Hex.GFqRing.instSubPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Sub (PolyQuotient f hf)

Equations

• Hex.GFqRing.instSubPolyQuotient = { sub := Hex.GFqRing.sub }

@[instance_reducible]

instance Hex.GFqRing.instPowPolyQuotientNat {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Pow (PolyQuotient f hf) Nat

Equations

• Hex.GFqRing.instPowPolyQuotientNat = { pow := Hex.GFqRing.pow }

@[instance_reducible]

instance Hex.GFqRing.instNatCastPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : NatCast (PolyQuotient f hf)

Equations

• Hex.GFqRing.instNatCastPolyQuotient = { natCast := Hex.GFqRing.natCast f hf }

@[instance_reducible]

instance Hex.GFqRing.instOfNatPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) : OfNat (PolyQuotient f hf) n

Equations

• Hex.GFqRing.instOfNatPolyQuotient n = { ofNat := Hex.GFqRing.natCast f hf n }

@[instance_reducible]

instance Hex.GFqRing.instSMulNatPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : SMul Nat (PolyQuotient f hf)

Equations

• Hex.GFqRing.instSMulNatPolyQuotient = { smul := Hex.GFqRing.nsmul }

@[instance_reducible]

instance Hex.GFqRing.instIntCastPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : IntCast (PolyQuotient f hf)

Equations

• Hex.GFqRing.instIntCastPolyQuotient = { intCast := Hex.GFqRing.intCast f hf }

@[instance_reducible]

instance Hex.GFqRing.instSMulIntPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : SMul Int (PolyQuotient f hf)

Equations

• Hex.GFqRing.instSMulIntPolyQuotient = { smul := Hex.GFqRing.zsmul }

@[simp]

theorem Hex.GFqRing.repr_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) : repr 0 = reduceMod f 0

The canonical representative of the quotient zero is the reduction of 0.

@[simp]

theorem Hex.GFqRing.repr_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) : repr 1 = reduceMod f 1

The multiplicative-identity representative is the reduction of 1.

@[simp]

theorem Hex.GFqRing.repr_const {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (c : ZMod64 p) : repr (const f hf c) = reduceMod f (FpPoly.C c)

The canonical representative of a constant quotient element is the reduction of C c.

theorem Hex.GFqRing.zero_ne_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) : 0 ≠ 1

Modulo any nonconstant polynomial, the zero and one quotient elements are distinct.

@[simp]

theorem Hex.GFqRing.natCast_eq_const {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (n : Nat) : natCast f hf n = const f hf ↑n

natCast unfolds to the corresponding constant quotient element.

@[simp]

theorem Hex.GFqRing.repr_natCast {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (n : Nat) : repr (natCast f hf n) = reduceMod f (FpPoly.C ↑n)

The canonical representative of natCast n is the reduction of C (n : ZMod64 p).

theorem Hex.GFqRing.natCast_eq_of_zmod64_natCast_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) {m n : Nat} (h : ↑m = ↑n) : ↑m = ↑n

Two natural-number casts coincide in the quotient ring whenever their prime-field casts do.

theorem Hex.GFqRing.natCast_eq_of_mod_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) {m n : Nat} (h : m % p = n % p) : ↑m = ↑n

Two natural-number casts coincide in the quotient ring whenever they agree modulo p.

theorem Hex.GFqRing.natCast_eq_natCast_iff_reduceMod_const_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (m n : Nat) : ↑m = ↑n ↔ reduceMod f (FpPoly.C ↑m) = reduceMod f (FpPoly.C ↑n)

Equality of natural-number casts is equivalent to equality of the underlying reduced constant polynomials. Internal stepping stone toward natCast_eq_natCast_iff_mod_eq; the forward direction projects quotient-level natCast equality to reduceMod-level equality.

theorem Hex.GFqRing.natCast_eq_natCast_iff_mod_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (m n : Nat) : ↑m = ↑n ↔ m % p = n % p

Equality of natural-number casts in the quotient ring is exactly equality modulo p. This is the user-facing iff form (consumed for example by Lean.Grind.IsCharP on the field layer); the reverse direction reduces to natCast_eq_of_mod_eq.

@[simp]

theorem Hex.GFqRing.repr_add {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : repr (x + y) = reduceMod f (repr x + repr y)

The canonical representative of a sum reduces the sum of representatives.

@[simp]

theorem Hex.GFqRing.repr_mul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : repr (x * y) = reduceMod f (repr x * repr y)

The canonical representative of a product reduces the product of representatives.

@[simp]

theorem Hex.GFqRing.repr_neg {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (-x) = reduceMod f (-repr x)

The canonical representative of a negation reduces the negation of the representative.

@[simp]

theorem Hex.GFqRing.repr_sub {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : repr (x - y) = reduceMod f (repr x - repr y)

The canonical representative of a difference reduces the difference of representatives.

@[simp]

theorem Hex.GFqRing.repr_pow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) (n : Nat) : repr (x ^ n) = repr (pow x n)

Quotient exponentiation via the Pow instance agrees with the internal pow definition.

def Hex.GFqRing.linearPow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : Nat → PolyQuotient f hf

Proof-only linear recurrence x^(n+1) = x^n * x, used to discharge the pow_zero / pow_succ fields of the Lean.Grind.Semiring instance. The executable pow is square-and-multiply (O(log n)); pow_eq_linearPow ties the two together.

Equations

• Hex.GFqRing.linearPow x 0 = 1
• Hex.GFqRing.linearPow x n.succ = Hex.GFqRing.linearPow x n * x

@[simp]

theorem Hex.GFqRing.ofPoly_zero_eq_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) : ofPoly f hf 0 = 0

ofPoly applied to the zero polynomial yields the canonical zero quotient element.

@[simp]

theorem Hex.GFqRing.ofPoly_one_eq_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) : ofPoly f hf 1 = 1

ofPoly applied to the one polynomial yields the canonical one quotient element.

@[simp]

theorem Hex.GFqRing.ofPoly_const_eq_const {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (c : ZMod64 p) : ofPoly f hf (FpPoly.C c) = const f hf c

ofPoly applied to a constant polynomial agrees with const.

@[simp]

theorem Hex.GFqRing.repr_neg_ofPoly {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (a : FpPoly p) : repr (-ofPoly f hf a) = reduceMod f (-reduceMod f a)

The representative of a negated constructed quotient element is the canonical reduction of the negated canonical representative.

@[simp]

theorem Hex.GFqRing.repr_sub_ofPoly {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (a b : FpPoly p) : repr (ofPoly f hf a - ofPoly f hf b) = reduceMod f (reduceMod f a - reduceMod f b)

The representative of a difference of constructed quotient elements is the canonical reduction of the difference of their canonical representatives.

theorem Hex.GFqRing.repr_add_comm {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : repr (x + y) = repr (y + x)

Representative-level commutativity of addition used by quotient additive reasoning.

theorem Hex.GFqRing.repr_zero_mul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (0 * x) = 0

Representative-level left zero multiplication used by the quotient semiring instance.

theorem Hex.GFqRing.repr_mul_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (x * 0) = 0

Representative-level right zero multiplication used by the quotient semiring instance.

theorem Hex.GFqRing.repr_mul_comm {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : repr (x * y) = repr (y * x)

Representative-level commutativity of multiplication used by the quotient commutative ring instance.

theorem Hex.GFqRing.natCast_succ {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (n : Nat) : OfNat.ofNat (n + 1) = OfNat.ofNat n + 1

The OfNat literal at n + 1 decomposes as the OfNat literal at n plus one in the quotient ring. Witnesses the Lean.Grind.Semiring.natCast_succ axiom field.

@[simp]

theorem Hex.GFqRing.intCast_ofNat {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (n : Nat) : intCast f hf (Int.ofNat n) = natCast f hf n

Integer cast of a non-negative integer unfolds to the corresponding natCast.

@[simp]

theorem Hex.GFqRing.intCast_negSucc {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (n : Nat) : intCast f hf (Int.negSucc n) = -natCast f hf (n + 1)

Integer cast of -(n + 1) is the negation of the (n + 1) natural-number cast.

@[simp]

theorem Hex.GFqRing.repr_intCast_ofNat {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (n : Nat) : repr (intCast f hf (Int.ofNat n)) = reduceMod f (FpPoly.C ↑n)

Canonical representative of intCast (Int.ofNat n) is the reduction of C (n : ZMod64 p).

@[simp]

theorem Hex.GFqRing.repr_intCast_negSucc {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (n : Nat) : repr (intCast f hf (Int.negSucc n)) = reduceMod f (-reduceMod f (FpPoly.C ↑(n + 1)))

Canonical representative of intCast (Int.negSucc n) is the reduction of the negation of the reduced C (n + 1 : ZMod64 p). The double reduceMod is the projection of the negation of the canonical natCast representative.

@[simp]

theorem Hex.GFqRing.zsmul_ofNat {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) (x : PolyQuotient f hf) : zsmul (Int.ofNat n) x = nsmul n x

Integer scalar multiplication by a non-negative integer unfolds to natural scalar multiplication.

@[simp]

theorem Hex.GFqRing.zsmul_negSucc {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) (x : PolyQuotient f hf) : zsmul (Int.negSucc n) x = -nsmul (n + 1) x

Integer scalar multiplication by -(n + 1) is the negation of the (n + 1) natural scalar multiplication.

@[simp]

theorem Hex.GFqRing.repr_zsmul_ofNat {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) (x : PolyQuotient f hf) : repr (zsmul (Int.ofNat n) x) = repr (nsmul n x)

Canonical representative of zsmul (Int.ofNat n) x reduces to the nsmul-level representative.

@[simp]

theorem Hex.GFqRing.repr_zsmul_negSucc {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) (x : PolyQuotient f hf) : repr (zsmul (Int.negSucc n) x) = reduceMod f (-repr (nsmul (n + 1) x))

Canonical representative of zsmul (Int.negSucc n) x is the reduction of the negation of the (n + 1) natural scalar multiplication's representative.

theorem Hex.GFqRing.neg_zero_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : -0 = 0

Negation of the quotient zero is the quotient zero. Used by neg_zsmul_eq and intCast_neg_eq (the Lean.Grind.Ring.neg_zsmul / intCast_neg axiom witnesses) for the boundary n = 0 case.

theorem Hex.GFqRing.reduceMod_mul_reduceMod {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f a b : FpPoly p) : reduceMod f (a * b) = reduceMod f (reduceMod f a * reduceMod f b)

Public alias for reduceMod_mul_reduceMod_congr: reducing both factors before quotient reduction preserves the canonical representative.

@[simp]

theorem Hex.GFqRing.reduceMod_repr {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : reduceMod f (repr x) = repr x

The canonical representative of a quotient element is already reduced.

@[simp]

theorem Hex.GFqRing.repr_add_ofPoly {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (a b : FpPoly p) : repr (ofPoly f hf a + ofPoly f hf b) = reduceMod f (a + b)

The representative of a sum of constructed quotient elements is the canonical reduction of the unreduced polynomial sum. This is the simp normal form for addition through ofPoly.

@[simp]

theorem Hex.GFqRing.repr_mul_ofPoly {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (a b : FpPoly p) : repr (ofPoly f hf a * ofPoly f hf b) = reduceMod f (a * b)

The representative of a product of constructed quotient elements is the canonical reduction of the unreduced polynomial product. This is the simp normal form for multiplication through ofPoly.

theorem Hex.GFqRing.repr_zero_add {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (0 + x) = repr x

Representative-level left-zero law used to build the quotient Lean.Grind.Semiring.

theorem Hex.GFqRing.repr_add_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (x + 0) = repr x

Representative-level right-zero law used to build the quotient Lean.Grind.Semiring.

theorem Hex.GFqRing.repr_add_assoc {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y z : PolyQuotient f hf) : repr (x + y + z) = repr (x + (y + z))

Representative-level associativity of addition used to build the quotient Lean.Grind.Semiring.

theorem Hex.GFqRing.repr_one_mul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (1 * x) = repr x

Representative-level left identity law for multiplication used by the quotient semiring instance.

theorem Hex.GFqRing.repr_mul_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (x * 1) = repr x

Representative-level right identity law for multiplication used by the quotient semiring instance.

theorem Hex.GFqRing.repr_mul_assoc {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y z : PolyQuotient f hf) : repr (x * y * z) = repr (x * (y * z))

Representative-level associativity of multiplication used to build the quotient Lean.Grind.Semiring.

theorem Hex.GFqRing.repr_left_distrib {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y z : PolyQuotient f hf) : repr (x * (y + z)) = repr (x * y + x * z)

Representative-level left distributivity used to build the quotient Lean.Grind.Semiring.

theorem Hex.GFqRing.repr_right_distrib {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y z : PolyQuotient f hf) : repr ((x + y) * z) = repr (x * z + y * z)

Representative-level right distributivity used to build the quotient Lean.Grind.Semiring.

theorem Hex.GFqRing.repr_neg_add_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (-x + x) = 0

Representative-level left inverse law used to build the quotient Lean.Grind.Ring.

theorem Hex.GFqRing.sub_eq_add_neg {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x y : PolyQuotient f hf) : x - y = x + -y

Quotient-level subtraction law used directly by the Lean.Grind.Ring instance.

@[simp]

theorem Hex.GFqRing.nsmul_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : nsmul 0 x = 0

Unfolded base of the nsmul recurrence: zero scalar multiplication yields the quotient zero. The implementation nsmul.go runs binary decomposition (via linearNSmul); this lemma exposes the textbook recurrence shape that Lean.Grind.Semiring's nsmul_zero axiom field consumes.

@[simp]

theorem Hex.GFqRing.nsmul_succ {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) (x : PolyQuotient f hf) : nsmul (n + 1) x = nsmul n x + x

Unfolded step of the nsmul recurrence. This is a theorem about the projected behaviour, not the implementation strategy: nsmul.go uses binary decomposition (via linearNSmul_double / linearNSmul_double_add_one) instead of textbook n+1 ↦ pred + 1 recursion. Consumed by Lean.Grind.Semiring's nsmul_succ axiom field.

@[simp]

theorem Hex.GFqRing.repr_nsmul_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : repr (nsmul 0 x) = reduceMod f 0

Canonical representative of nsmul 0 x is the reduction of 0.

@[simp]

theorem Hex.GFqRing.repr_nsmul_succ {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) (x : PolyQuotient f hf) : repr (nsmul (n + 1) x) = reduceMod f (repr (nsmul n x) + repr x)

Canonical representative of nsmul (n + 1) x is the reduction of the sum of the previous nsmul's representative and repr x.

theorem Hex.GFqRing.nsmul_eq_natCast_mul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (n : Nat) (x : PolyQuotient f hf) : n • x = ↑n * x

Natural scalar multiplication agrees with multiplication by the corresponding natCast. Witnesses the Lean.Grind.Semiring.nsmul_eq_natCast_mul axiom field.

theorem Hex.GFqRing.neg_neg_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) : - -x = x

Double negation in the quotient ring is the identity. Proved by the textbook additive-group calculation -(-x) = -(-x) + (-x + x) = (-(-x) + -x) + x = 0 + x = x. Used by neg_zsmul_eq and intCast_neg_eq for the Int.negSucc case.

theorem Hex.GFqRing.neg_zsmul_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (i : Int) (a : PolyQuotient f hf) : -i • a = -(i • a)

Negation distributes over integer scalar multiplication. Witnesses the Lean.Grind.Ring.neg_zsmul axiom field. The three branches handle i = Int.ofNat 0, i = Int.ofNat (n + 1), and i = Int.negSucc n separately because Int.neg evaluates differently on each.

theorem Hex.GFqRing.intCast_neg_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (i : Int) : ↑(-i) = -↑i

Negation distributes over integer cast. Witnesses the Lean.Grind.Ring.intCast_neg axiom field. Three branches mirror neg_zsmul_eq.

theorem Hex.GFqRing.pow_eq_linearPow {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} (x : PolyQuotient f hf) (n : Nat) : pow x n = linearPow x n

The executable square-and-multiply pow returns the same element as the proof-only linear recurrence linearPow. The Lean.Grind.Semiring instance rewrites by this equality to discharge its pow_succ field.

@[instance_reducible]

instance Hex.GFqRing.instSemiringPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Lean.Grind.Semiring (PolyQuotient f hf)

Equations

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

@[instance_reducible]

instance Hex.GFqRing.instRingPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Lean.Grind.Ring (PolyQuotient f hf)

Equations

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

@[instance_reducible]

instance Hex.GFqRing.instCommRingPolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} {hf : 0 < f.degree} : Lean.Grind.CommRing (PolyQuotient f hf)

Equations

• Hex.GFqRing.instCommRingPolyQuotient = { toRing := Hex.GFqRing.instRingPolyQuotient, mul_comm := ⋯ }