def Hex.GFqField.natCast {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) (n : Nat) : FiniteField f hf hp hirr

Natural-number literals reuse the quotient-ring cast and then rewrap the resulting reduced residue.

Equations

• Hex.GFqField.natCast f hf hp hirr n = Hex.GFqField.ofQuotient ↑n

def Hex.GFqField.zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) : FiniteField f hf hp hirr

The additive identity in the finite-field wrapper.

Equations

• Hex.GFqField.zero f hf hp hirr = Hex.GFqField.ofQuotient 0

def Hex.GFqField.one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) : FiniteField f hf hp hirr

The multiplicative identity in the finite-field wrapper.

Equations

• Hex.GFqField.one f hf hp hirr = Hex.GFqField.ofQuotient 1

def Hex.GFqField.add {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

Field addition reuses the quotient-ring sum.

Equations

• Hex.GFqField.add x y = Hex.GFqField.ofQuotient (x.toQuotient + y.toQuotient)

def Hex.GFqField.mul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

Field multiplication reuses the quotient-ring product.

Equations

• Hex.GFqField.mul x y = Hex.GFqField.ofQuotient (x.toQuotient * y.toQuotient)

def Hex.GFqField.neg {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

Field negation reuses the quotient-ring additive inverse.

Equations

• Hex.GFqField.neg x = Hex.GFqField.ofQuotient (-x.toQuotient)

def Hex.GFqField.sub {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

Field subtraction reuses the quotient-ring difference.

Equations

• Hex.GFqField.sub x y = Hex.GFqField.ofQuotient (x.toQuotient - y.toQuotient)

def Hex.GFqField.pow {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) (n : Nat) : FiniteField f hf hp hirr

Exponentiation reuses the quotient-ring repeated-multiplication path.

Equations

• Hex.GFqField.pow x n = Hex.GFqField.ofQuotient (x.toQuotient ^ n)

def Hex.GFqField.nsmul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (n : Nat) (x : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

Natural scalar multiplication reuses the quotient-ring scalar action.

Equations

• Hex.GFqField.nsmul n x = Hex.GFqField.ofQuotient (n • x.toQuotient)

def Hex.GFqField.intCast {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) (i : Int) : FiniteField f hf hp hirr

Integer literals reuse the quotient-ring cast and then rewrap the reduced residue.

Equations

• Hex.GFqField.intCast f hf hp hirr i = Hex.GFqField.ofQuotient ↑i

def Hex.GFqField.zsmul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (i : Int) (x : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

Integer scalar multiplication reuses the quotient-ring scalar action.

Equations

• Hex.GFqField.zsmul i x = Hex.GFqField.ofQuotient (i • x.toQuotient)

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

The inverse polynomial representative for a quotient element.

This normalizes the extended-GCD left coefficient by the gcd's constant-unit factor, producing a polynomial whose residue is the multiplicative inverse whenever the quotient element is nonzero.

At zero this is not an inverse and does not claim to be: the extended GCD of 0 and f returns f itself, so the result is f scaled by the inverse of its own constant coefficient. It stays public because inv is @[expose] and mentions it, but inv decides the zero case before reaching it, and callers should reason through the field-level lemmas below rather than by unfolding this.

Equations

• Hex.GFqField.invPoly x = Hex.DensePoly.scale ((Hex.DensePoly.xgcd (Hex.GFqRing.repr x) f).gcd.coeff 0)⁻¹ (Hex.DensePoly.xgcd (Hex.GFqRing.repr x) f).left

def Hex.GFqField.inv {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

Field inversion stays on the quotient-reduction path by reusing the polynomial extended-GCD witness, normalized by the gcd's constant unit factor. The 0 case follows the usual junk-value convention required by Lean.Grind.Field.

Equations

• Hex.GFqField.inv x = if _hx : x = Hex.GFqField.zero f hf hp hirr then Hex.GFqField.zero f hf hp hirr else Hex.GFqField.ofPoly f hf hp hirr (Hex.GFqField.invPoly x.toQuotient)

def Hex.GFqField.div {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

Division is multiplication by the inverse candidate.

Equations

• Hex.GFqField.div x y = Hex.GFqField.mul x (Hex.GFqField.inv y)

def Hex.GFqField.zpow {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : Int → FiniteField f hf hp hirr

Integer exponentiation uses the existing natural-power path together with the inverse candidate for negative exponents.

Equations

• Hex.GFqField.zpow x (Int.ofNat n) = Hex.GFqField.pow x n
• Hex.GFqField.zpow x (Int.negSucc n) = Hex.GFqField.inv (Hex.GFqField.pow x (n + 1))

def Hex.GFqField.frob {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : FiniteField f hf hp hirr

The Frobenius map is the p-th power map on the existing quotient representation.

Equations

• Hex.GFqField.frob x = Hex.GFqField.pow x p

@[instance_reducible]

instance Hex.GFqField.instZeroFiniteField {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Zero (FiniteField f hf hp hirr)

Field-wrapper zero is backed by the quotient-ring zero.

Equations

• Hex.GFqField.instZeroFiniteField = { zero := Hex.GFqField.zero f hf hp hirr }

@[instance_reducible]

instance Hex.GFqField.instOneFiniteField {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : One (FiniteField f hf hp hirr)

Field-wrapper one is backed by the quotient-ring one.

Equations

• Hex.GFqField.instOneFiniteField = { one := Hex.GFqField.one f hf hp hirr }

@[instance_reducible]

instance Hex.GFqField.instAddFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Add (FiniteField f hf hp hirr)

Field-wrapper addition delegates to quotient-ring addition.

Equations

• Hex.GFqField.instAddFiniteField = { add := Hex.GFqField.add }

@[instance_reducible]

instance Hex.GFqField.instMulFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Mul (FiniteField f hf hp hirr)

Field-wrapper multiplication delegates to quotient-ring multiplication.

Equations

• Hex.GFqField.instMulFiniteField = { mul := Hex.GFqField.mul }

@[instance_reducible]

instance Hex.GFqField.instNegFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Neg (FiniteField f hf hp hirr)

Field-wrapper negation delegates to quotient-ring negation.

Equations

• Hex.GFqField.instNegFiniteField = { neg := Hex.GFqField.neg }

@[instance_reducible]

instance Hex.GFqField.instSubFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Sub (FiniteField f hf hp hirr)

Field-wrapper subtraction delegates to quotient-ring subtraction.

Equations

• Hex.GFqField.instSubFiniteField = { sub := Hex.GFqField.sub }

@[instance_reducible]

instance Hex.GFqField.instPowFiniteFieldNat {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Pow (FiniteField f hf hp hirr) Nat

Natural powers use the quotient-ring square-and-multiply path.

Equations

• Hex.GFqField.instPowFiniteFieldNat = { pow := Hex.GFqField.pow }

@[instance_reducible]

instance Hex.GFqField.instNatCastFiniteField {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : NatCast (FiniteField f hf hp hirr)

Natural literals are quotient-ring natural literals rewrapped as field elements.

Equations

• Hex.GFqField.instNatCastFiniteField = { natCast := Hex.GFqField.natCast f hf hp hirr }

@[instance_reducible]

instance Hex.GFqField.instOfNatFiniteField {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (n : Nat) : OfNat (FiniteField f hf hp hirr) n

OfNat literals use the field wrapper's natural-literal implementation.

Equations

• Hex.GFqField.instOfNatFiniteField n = { ofNat := Hex.GFqField.natCast f hf hp hirr n }

@[instance_reducible]

instance Hex.GFqField.instSMulNatFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : SMul Nat (FiniteField f hf hp hirr)

Natural scalar multiplication delegates to quotient-ring scalar multiplication.

Equations

• Hex.GFqField.instSMulNatFiniteField = { smul := Hex.GFqField.nsmul }

@[instance_reducible]

instance Hex.GFqField.instIntCastFiniteField {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : IntCast (FiniteField f hf hp hirr)

Integer literals are quotient-ring integer literals rewrapped as field elements.

Equations

• Hex.GFqField.instIntCastFiniteField = { intCast := Hex.GFqField.intCast f hf hp hirr }

@[instance_reducible]

instance Hex.GFqField.instSMulIntFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : SMul Int (FiniteField f hf hp hirr)

Integer scalar multiplication delegates to quotient-ring scalar multiplication.

Equations

• Hex.GFqField.instSMulIntFiniteField = { smul := Hex.GFqField.zsmul }

@[instance_reducible]

instance Hex.GFqField.instInvFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Inv (FiniteField f hf hp hirr)

Field inversion uses the wrapper's extended-GCD inverse.

Equations

• Hex.GFqField.instInvFiniteField = { inv := Hex.GFqField.inv }

@[instance_reducible]

instance Hex.GFqField.instDivFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Div (FiniteField f hf hp hirr)

Field division is the wrapper's multiplication-by-inverse operation.

Equations

• Hex.GFqField.instDivFiniteField = { div := Hex.GFqField.div }

@[instance_reducible]

instance Hex.GFqField.instHPowFiniteFieldInt {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : HPow (FiniteField f hf hp hirr) Int (FiniteField f hf hp hirr)

Integer powers use natural powers for nonnegative exponents and inversion for negative ones.

Equations

• Hex.GFqField.instHPowFiniteFieldInt = { hPow := Hex.GFqField.zpow }

@[simp]

theorem Hex.GFqField.toQuotient_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) : FiniteField.toQuotient 0 = 0

Zero projects to the quotient-ring zero.

@[simp]

theorem Hex.GFqField.toQuotient_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) : FiniteField.toQuotient 1 = 1

One projects to the quotient-ring one.

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

The quotient-field wrapper is nontrivial.

@[simp]

theorem Hex.GFqField.toQuotient_natCast {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) (n : Nat) : (↑n).toQuotient = ↑n

Natural literals project to quotient-ring natural literals.

@[simp]

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

The representative of a natural literal is the reduced constant polynomial.

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

Equal ZMod64 residues give equal natural literals in the field wrapper.

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

Equal residues modulo p give equal natural literals in the field wrapper.

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

Equality of natural literals is equivalent to equality of their reduced constants.

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

Equality of natural literals is equivalent to congruence modulo p.

@[simp]

theorem Hex.GFqField.toQuotient_add {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : (x + y).toQuotient = x.toQuotient + y.toQuotient

Addition projects to quotient-ring addition.

@[simp]

theorem Hex.GFqField.toQuotient_mul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : (x * y).toQuotient = x.toQuotient * y.toQuotient

Multiplication projects to quotient-ring multiplication.

@[simp]

theorem Hex.GFqField.toQuotient_neg {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : (-x).toQuotient = -x.toQuotient

Negation projects to the quotient-ring additive inverse.

@[simp]

theorem Hex.GFqField.toQuotient_sub {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : (x - y).toQuotient = x.toQuotient - y.toQuotient

Subtraction projects to the quotient-ring difference.

@[simp]

theorem Hex.GFqField.toQuotient_nsmul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (n : Nat) (x : FiniteField f hf hp hirr) : (n • x).toQuotient = n • x.toQuotient

Natural scalar multiplication projects to the quotient-ring scalar action.

@[simp]

theorem Hex.GFqField.toQuotient_intCast {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) (i : Int) : (↑i).toQuotient = ↑i

Integer literals project to quotient-ring integer literals.

@[simp]

theorem Hex.GFqField.toQuotient_zsmul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (i : Int) (x : FiniteField f hf hp hirr) : (i • x).toQuotient = i • x.toQuotient

Integer scalar multiplication projects to the quotient-ring scalar action.

@[simp]

theorem Hex.GFqField.toQuotient_pow {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) (n : Nat) : (x ^ n).toQuotient = x.toQuotient ^ n

Natural powers project to quotient-ring natural powers.

@[simp]

theorem Hex.GFqField.toQuotient_div {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : (x / y).toQuotient = x.toQuotient * (inv y).toQuotient

Division projects to multiplication by the projected inverse.

@[simp]

theorem Hex.GFqField.toQuotient_zpow_ofNat {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) (n : Nat) : (x ^ Int.ofNat n).toQuotient = x.toQuotient ^ n

Nonnegative integer powers project to quotient-ring natural powers.

@[simp]

theorem Hex.GFqField.toQuotient_zpow_negSucc {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) (n : Nat) : (x ^ Int.negSucc n).toQuotient = (inv (pow x (n + 1))).toQuotient

Negative integer powers project through inversion of the positive power.

@[simp]

theorem Hex.GFqField.inv_zero {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) : 0⁻¹ = 0

The field inverse uses the standard junk value at zero.

@[simp]

theorem Hex.GFqField.div_eq_mul_inv {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : x / y = x * y⁻¹

Division is field multiplication by inverse.

theorem Hex.GFqField.mul_inv_cancel {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} {x : FiniteField f hf hp hirr} (hx : x ≠ 0) : x * x⁻¹ = 1

A nonzero field element cancels against its inverse on the right.

theorem Hex.GFqField.inv_mul_cancel {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} {x : FiniteField f hf hp hirr} (hx : x ≠ 0) : x⁻¹ * x = 1

A nonzero field element cancels against its inverse on the left.

@[simp]

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

The additive-identity representative is the reduced form of 0.

@[simp]

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

The multiplicative-identity representative is the reduced form of 1.

@[simp]

theorem Hex.GFqField.repr_add {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : repr (x + y) = GFqRing.reduceMod f (repr x + repr y)

The representative of a sum is the reduced sum of representatives.

@[simp]

theorem Hex.GFqField.repr_mul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : repr (x * y) = GFqRing.reduceMod f (repr x * repr y)

The representative of a product is the reduced product of representatives.

@[simp]

theorem Hex.GFqField.repr_neg {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : repr (-x) = GFqRing.reduceMod f (-repr x)

The representative of a negation reduces from the negated representative.

@[simp]

theorem Hex.GFqField.repr_sub {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : repr (x - y) = GFqRing.reduceMod f (repr x - repr y)

The representative of a subtraction reduces from the difference of representatives.

@[simp]

theorem Hex.GFqField.repr_pow {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) (n : Nat) : repr (x ^ n) = GFqRing.repr (x.toQuotient ^ n)

The representative of a natural power is the quotient-ring power representative.

@[simp]

theorem Hex.GFqField.repr_div {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x y : FiniteField f hf hp hirr) : repr (x / y) = GFqRing.repr (x.toQuotient * (inv y).toQuotient)

The representative of a quotient is the quotient-ring product with the projected inverse.

@[simp]

theorem Hex.GFqField.repr_zpow_ofNat {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) (n : Nat) : repr (x ^ Int.ofNat n) = GFqRing.repr (x.toQuotient ^ n)

Nonnegative integer powers share the natural-power representative.

@[simp]

theorem Hex.GFqField.repr_zpow_negSucc {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) (n : Nat) : repr (x ^ Int.negSucc n) = GFqRing.repr (inv (pow x (n + 1))).toQuotient

Negative integer powers represent the inverse of the corresponding positive power.

@[simp]

theorem Hex.GFqField.repr_intCast {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (hp : Nat.Prime p) (hirr : f.Irreducible) (i : Int) : repr ↑i = GFqRing.repr ↑i

The representative of an integer cast lifts the quotient-ring cast.

@[simp]

theorem Hex.GFqField.repr_nsmul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (n : Nat) (x : FiniteField f hf hp hirr) : repr (n • x) = GFqRing.repr (n • x.toQuotient)

The representative of a natural scalar action lifts the quotient-ring action.

@[simp]

theorem Hex.GFqField.repr_zsmul {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (i : Int) (x : FiniteField f hf hp hirr) : repr (i • x) = GFqRing.repr (i • x.toQuotient)

The representative of an integer scalar action lifts the quotient-ring action.

@[instance_reducible]

instance Hex.GFqField.instSemiringFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Lean.Grind.Semiring (FiniteField f hf hp hirr)

Semiring laws for finite-field elements, transported from the quotient ring.

Equations

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

@[instance_reducible]

instance Hex.GFqField.instRingFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Lean.Grind.Ring (FiniteField f hf hp hirr)

Ring laws for finite-field elements, transported from the quotient ring.

Equations

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

@[instance_reducible]

instance Hex.GFqField.instCommRingFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Lean.Grind.CommRing (FiniteField f hf hp hirr)

Commutative multiplication for finite-field elements, inherited from the quotient ring.

Equations

• Hex.GFqField.instCommRingFiniteField = { toRing := Hex.GFqField.instRingFiniteField, mul_comm := ⋯ }

theorem Hex.GFqField.inv_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : 1⁻¹ = 1

The inverse of 1 is 1, since 1 * 1 = 1; a normalization step in the field-structure proofs.

theorem Hex.GFqField.inv_inv {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : x⁻¹⁻¹ = x

Double inverse is the identity: x⁻¹⁻¹ = x; obtained from inverse uniqueness via the cancellation x⁻¹ * x = 1, with the zero case handled separately.

theorem Hex.GFqField.inv_inv_def {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : (inv x)⁻¹ = x

Double inverse stated through the inv-named function: (inv x)⁻¹ = x; the form consumed where the explicit inv definition appears rather than the ⁻¹ notation.

theorem Hex.GFqField.pow_zero_eq_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : pow x 0 = 1

The empty product pow x 0 = 1; the base case anchoring the exponentiation recursion in the FiniteField power API.

@[instance_reducible]

instance Hex.GFqField.instFieldFiniteField {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Lean.Grind.Field (FiniteField f hf hp hirr)

Field laws for finite-field elements, using the field-level inverse lemmas.

Equations

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

instance Hex.GFqField.instIsCharPFiniteField {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} : Lean.Grind.IsCharP (FiniteField f hf hp hirr) p

Characteristic-p automation for natural literals in the finite field.

theorem Hex.GFqField.frob_eq_pow {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : frob x = x ^ p

Frobenius is definitionally the p-th power map.

@[simp]

theorem Hex.GFqField.toQuotient_frob {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : (frob x).toQuotient = x.toQuotient ^ p

Frobenius projects to the quotient-ring p-th power.

@[simp]

theorem Hex.GFqField.repr_frob {p : Nat} [ZMod64.Bounds p] {hp : Nat.Prime p} {f : FpPoly p} {hf : 0 < f.degree} {hirr : f.Irreducible} (x : FiniteField f hf hp hirr) : repr (frob x) = GFqRing.repr (x.toQuotient ^ p)

The representative of Frobenius is the quotient-ring p-th power representative.