def HexGFqMathlib.FpPoly.coeffIndex {p : ℕ} [Hex.ZMod64.Bounds p] (degree : ℕ) (f : Hex.FpPoly p) : ℕ

Interpret the first degree coefficients of an FpPoly as a base-p index.

This is the encoder half of the bijection between degree-< degree polynomials and Fin (p ^ degree); ofIndexBelowDegree is its inverse on bounded inputs (coeffIndex_ofIndexBelowDegree, ofIndexBelowDegree_coeffIndex), and the value is always below p ^ degree (coeffIndex_lt).

Equations

• HexGFqMathlib.FpPoly.coeffIndex degree f = List.foldl (fun (acc i : ℕ) => acc + (Hex.DensePoly.coeff f i).toNat * p ^ i) 0 (List.range degree)

def HexGFqMathlib.FpPoly.ofIndexBelowDegree {p : ℕ} [Hex.ZMod64.Bounds p] (degree index : ℕ) : Hex.FpPoly p

Decode a base-p index into a polynomial with at most degree coefficients.

The decoder half of the coeffIndex bijection. Its coefficients are characterised by coeff_ofIndexBelowDegree_of_lt (in range, a simp normal form) and coeff_ofIndexBelowDegree_of_ge (beyond the width, zero), and its FpPoly.degree stays below degree when the width is positive (ofIndexBelowDegree_degree_lt).

Equations

• HexGFqMathlib.FpPoly.ofIndexBelowDegree degree index = Hex.FpPoly.ofCoeffs (List.map (fun (i : ℕ) => Hex.ZMod64.ofNat p (index / p ^ i)) (List.range degree)).toArray

theorem HexGFqMathlib.FpPoly.coeffIndex_succ {p : ℕ} [Hex.ZMod64.Bounds p] (degree : ℕ) (f : Hex.FpPoly p) : coeffIndex (degree + 1) f = coeffIndex degree f + (Hex.DensePoly.coeff f degree).toNat * p ^ degree

Peeling the top position of the base-p encoding.

theorem HexGFqMathlib.FpPoly.coeffIndex_eq_ofDigits {p : ℕ} [Hex.ZMod64.Bounds p] (degree : ℕ) (f : Hex.FpPoly p) : coeffIndex degree f = Nat.ofDigits p (List.map (fun (i : ℕ) => (Hex.DensePoly.coeff f i).toNat) (List.range degree))

coeffIndex is the base-p interpretation of the per-position residue digits, exposing Mathlib's Nat.ofDigits API.

theorem HexGFqMathlib.FpPoly.coeffIndex_lt {p : ℕ} [Hex.ZMod64.Bounds p] (degree : ℕ) (f : Hex.FpPoly p) : coeffIndex degree f < p ^ degree

A base-p positional sum of degree residue digits stays below p ^ degree.

theorem HexGFqMathlib.FpPoly.ofDigits_div_pow_mod {p : ℕ} (hp : 0 < p) (L : List ℕ) (hL : ∀ x ∈ L, x < p) (j : ℕ) (hj : j < L.length) : Nat.ofDigits p L / p ^ j % p = L.getD j 0

Extracting digit j of a base-p number presented through Nat.ofDigits.

theorem HexGFqMathlib.FpPoly.ofDigits_range_map_div_pow_mod {p : ℕ} (hp : 0 < p) (degree n : ℕ) : n < p ^ degree → Nat.ofDigits p (List.map (fun (i : ℕ) => n / p ^ i % p) (List.range degree)) = n

Reconstructing a number below p ^ degree from its fixed-width base-p digits.

@[simp]

theorem HexGFqMathlib.FpPoly.coeff_ofIndexBelowDegree_of_lt {p : ℕ} [Hex.ZMod64.Bounds p] (degree index i : ℕ) (hi : i < degree) : Hex.DensePoly.coeff (ofIndexBelowDegree degree index) i = Hex.ZMod64.ofNat p (index / p ^ i)

Coefficients below the width read back the encoded base-p digit.

@[simp]

theorem HexGFqMathlib.FpPoly.coeff_ofIndexBelowDegree_of_ge {p : ℕ} [Hex.ZMod64.Bounds p] (degree index i : ℕ) (hi : degree ≤ i) : Hex.DensePoly.coeff (ofIndexBelowDegree degree index) i = 0

Coefficients at or beyond the width vanish.

theorem HexGFqMathlib.FpPoly.degree_lt_of_size_le {p : ℕ} [Hex.ZMod64.Bounds p] (g : Hex.FpPoly p) (d : ℕ) (hsz : Hex.DensePoly.size g ≤ d) (hd : 0 < d) : g.degree < d

The width-degree decoder produces a polynomial of size at most degree, hence degree below degree whenever the width is positive.

theorem HexGFqMathlib.FpPoly.size_le_degree_succ {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : Hex.DensePoly.size f ≤ f.degree + 1

A polynomial's stored size is at most one more than its FpPoly.degree.

theorem HexGFqMathlib.FpPoly.coeffIndex_lt_of_degree_lt {p : ℕ} [Hex.ZMod64.Bounds p] {degree : ℕ} {f : Hex.FpPoly p} (_hdeg : f.degree < degree) : coeffIndex degree f < p ^ degree

Bounded reduced polynomials encode to indices below p ^ degree.

theorem HexGFqMathlib.FpPoly.ofIndexBelowDegree_degree_lt {p : ℕ} [Hex.ZMod64.Bounds p] (degree index : ℕ) (hd : 0 < degree) : (ofIndexBelowDegree degree index).degree < degree

Decoded indices are represented by polynomials with degree below the requested bound. The positivity hypothesis is necessary: at degree = 0 the index type Fin (p ^ 0) = Fin 1 is inhabited but the decoder returns the zero polynomial, whose FpPoly.degree is 0.

@[simp]

theorem HexGFqMathlib.FpPoly.coeffIndex_ofIndexBelowDegree {p : ℕ} [Hex.ZMod64.Bounds p] (degree : ℕ) (index : Fin (p ^ degree)) : coeffIndex degree (ofIndexBelowDegree degree ↑index) = ↑index

Encoding after decoding recovers the bounded index.

@[simp]

theorem HexGFqMathlib.FpPoly.ofIndexBelowDegree_coeffIndex {p : ℕ} [Hex.ZMod64.Bounds p] {degree : ℕ} {f : Hex.FpPoly p} (hdeg : f.degree < degree) : ofIndexBelowDegree degree (coeffIndex degree f) = f

Decoding after encoding recovers a polynomial already below the degree bound.

@[instance_reducible]

noncomputable instance HexGFqMathlib.FiniteField.field {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} : Field (Hex.GFqField.FiniteField f hf hp hirr)

The executable finite-field wrapper carries Mathlib's Field structure through the field laws already proved for the implementation-facing Lean.Grind.Field hierarchy.

Equations

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

@[reducible, inline]

abbrev HexGFqMathlib.FiniteField.ReducedRep {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : Type

Reduced polynomial representatives for the quotient by f.

Equations

• HexGFqMathlib.FiniteField.ReducedRep f = { g : Hex.FpPoly p // g.degree < f.degree }

def HexGFqMathlib.FiniteField.reducedRepEquiv {p : ℕ} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} : Hex.GFqField.FiniteField f hf hp hirr ≃ ReducedRep f

The executable finite-field wrapper is equivalent to its canonical reduced polynomial representatives.

Equations

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

def HexGFqMathlib.FiniteField.reducedRepFinEquiv {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) (hf : 0 < f.degree) : ReducedRep f ≃ Fin (p ^ f.degree)

Reduced representatives are indexed by Fin (p ^ degree f). The positive-degree hypothesis is needed for the decoder's degree bound (see FpPoly.ofIndexBelowDegree_degree_lt); it is supplied at every call site by the nonconstant-modulus assumption.

Equations

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

def HexGFqMathlib.FiniteField.finEquiv {p : ℕ} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} : Hex.GFqField.FiniteField f hf hp hirr ≃ Fin (p ^ f.degree)

Generic finite-field elements are equivalent to the expected finite index type.

Equations

• HexGFqMathlib.FiniteField.finEquiv = HexGFqMathlib.FiniteField.reducedRepEquiv.trans (HexGFqMathlib.FiniteField.reducedRepFinEquiv f hf)

@[instance_reducible]

noncomputable instance HexGFqMathlib.FiniteField.fintype {p : ℕ} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} : Fintype (Hex.GFqField.FiniteField f hf hp hirr)

The generic executable finite-field wrapper is finite.

Equations

• HexGFqMathlib.FiniteField.fintype = Fintype.ofEquiv (Fin (p ^ f.degree)) HexGFqMathlib.FiniteField.finEquiv.symm

@[simp]

theorem HexGFqMathlib.FiniteField.fintype_card {p : ℕ} [Hex.ZMod64.Bounds p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} : Fintype.card (Hex.GFqField.FiniteField f hf hp hirr) = p ^ f.degree

The generic executable finite-field wrapper has the expected cardinality.

@[instance_reducible]

noncomputable instance HexGFqMathlib.GFq.fintype {p n : ℕ} [Hex.ZMod64.Bounds p] (h : Hex.Conway.SupportedEntry p n) : Fintype (Hex.GFq p n h)

Canonical Conway-backed GFq values inherit the generic finite-field enumeration.

Equations

• HexGFqMathlib.GFq.fintype h = HexGFqMathlib.FiniteField.fintype

theorem HexGFqMathlib.GFq.fintype_card {p n : ℕ} [Hex.ZMod64.Bounds p] (h : Hex.Conway.SupportedEntry p n) : Fintype.card (Hex.GFq p n h) = p ^ (Hex.GFq.modulus h).degree

Cardinality of the canonical Conway-backed GFq in terms of its selected modulus degree.

theorem HexGFqMathlib.GFq.modulus_degree {p n : ℕ} [Hex.ZMod64.Bounds p] (h : Hex.Conway.SupportedEntry p n) : (Hex.GFq.modulus h).degree = n

The committed Conway modulus has the requested extension degree.

@[simp]

theorem HexGFqMathlib.GFq.conwayPoly_degree {p n : ℕ} [Hex.ZMod64.Bounds p] (h : Hex.Conway.SupportedEntry p n) : (Hex.Conway.conwayPoly p n h).degree = n

The committed Conway polynomial has the requested extension degree. This is the Conway.conwayPoly-phrased twin of modulus_degree: it is the form simp needs once the @[simp] lemma modulus_eq_conway has normalised GFq.modulus h to Conway.conwayPoly p n h, and together with FiniteField.fintype_card it drives Fintype.card (GFq p n h) to p ^ n.

@[simp]

theorem HexGFqMathlib.GFq.fintype_card_eq_pow {p n : ℕ} [Hex.ZMod64.Bounds p] (h : Hex.Conway.SupportedEntry p n) : Fintype.card (Hex.GFq p n h) = p ^ n

Cardinality of canonical GFq p n as p ^ n.

theorem HexGFqMathlib.GFq.card_eq_galoisField_card {p n : ℕ} [Hex.ZMod64.Bounds p] [Fact (Nat.Prime p)] (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) : Fintype.card (Hex.GFq p n h) = Nat.card (GaloisField p n)

Canonical Hex.GFq and Mathlib's GaloisField have matching cardinalities.

noncomputable def HexGFqMathlib.GFq.equivGaloisField {p n : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] [Fact (Nat.Prime p)] (h : Hex.Conway.SupportedEntry p n) (hn : n ≠ 0) : Hex.GFq p n h ≃+* GaloisField p n

Canonical Hex.GFq values are ring-equivalent to Mathlib's GaloisField with the same characteristic and extension degree.

Equations

• HexGFqMathlib.GFq.equivGaloisField h hn = FiniteField.ringEquivOfCardEq ⋯