structure Hex.GFqField.FiniteField {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hf : 0 < f.degree) (_hp : Nat.Prime p) (_hirr : f.Irreducible) : Type

Executable finite-field elements are a thin wrapper around quotient-ring residues modulo an irreducible polynomial.

• toQuotient : GFqRing.PolyQuotient f hf

  The underlying reduced quotient-ring residue backing this field element.

  GFqRing.PolyQuotient is a prime-modulus type, and the witness it needs is the _hp this structure already carries. Deriving the instance here rather than demanding it from callers keeps FiniteField's signature unchanged; ZMod64.PrimeModulus is a Prop-valued class, so this instance and any ambient one are definitionally equal.

@[instance_reducible]

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

Field equality is decidable, and decided by comparing canonical representatives: elements are wrappers around reduced quotient values, so equality of the wrapped values is equality of the elements.

Equations

• Hex.GFqField.instDecidableEqFiniteField x y = match decEq x.toQuotient y.toQuotient with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

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

Wrap a quotient-ring element as a finite-field element.

Equations

• Hex.GFqField.ofQuotient x = { toQuotient := x }

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

Reduce a polynomial into the finite field by reusing the quotient-ring constructor.

The prime-modulus instance the quotient needs is derived from this constructor's own hp, so callers holding only a primality proof do not have to supply it a second time.

Equations

• Hex.GFqField.ofPoly f hf hp hirr g = Hex.GFqField.ofQuotient (Hex.GFqRing.ofPoly f hf g)

def Hex.GFqField.repr {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) : FpPoly p

Project a finite-field element to its canonical polynomial representative.

Equations

• Hex.GFqField.repr x = Hex.GFqRing.repr x.toQuotient

@[simp]

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

Projecting a wrapped quotient element returns the original quotient.

@[simp]

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

Reducing a polynomial into the field projects to the quotient-ring reduction.

@[simp]

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

A wrapped quotient exposes the same canonical polynomial representative.

@[simp]

theorem Hex.GFqField.ofQuotient_toQuotient {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) : ofQuotient x.toQuotient = x

Rewrapping a field element through its quotient projection is the identity.

@[simp]

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

The representative of a polynomial coerced into the field is its reduced form.

@[simp]

theorem Hex.GFqField.degree_repr_lt_degree {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).degree < f.degree

Canonical field representatives are reduced below the modulus degree.

theorem Hex.GFqField.toQuotient_inj {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.toQuotient = y.toQuotient ↔ x = y

Equality of field elements is equality of their quotient representatives.

theorem Hex.GFqField.ext {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} (h : x.toQuotient = y.toQuotient) : x = y

Extensionality through quotient representatives.

theorem Hex.GFqField.ext_iff {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.toQuotient = y.toQuotient