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

The degree of a polynomial, defaulting to 0 for the zero polynomial.

Equations

• f.degree = Hex.DensePoly.natDegree f

@[simp]

theorem Hex.FpPoly.degree_C {p : Nat} [ZMod64.Bounds p] (c : ZMod64 p) : (C c).degree = 0

Constant polynomials have FpPoly.degree equal to 0.

def Hex.GFqRing.reduceMod {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : FpPoly p → FpPoly p

Canonical remainder reduction modulo f, using the existing division surface.

Equations

• Hex.GFqRing.reduceMod f g = (Hex.DensePoly.divMod g f).snd

theorem Hex.GFqRing.reduceMod_eq_self_of_degree_lt {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : g.degree < f.degree → reduceMod f g = g

A polynomial of degree strictly below the modulus is already its own canonical representative.

@[simp]

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

The zero polynomial is already canonical modulo any nonconstant modulus.

@[simp]

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

The one polynomial is already canonical modulo any nonconstant modulus.

def Hex.GFqRing.IsReduced {p : Nat} [ZMod64.Bounds p] (f g : FpPoly p) : Prop

Polynomials already known to be canonical representatives modulo f.

Equations

• Hex.GFqRing.IsReduced f g = ∃ (h : Hex.FpPoly p), g = Hex.GFqRing.reduceMod f h

@[reducible, inline]

abbrev Hex.GFqRing.PolyQuotient {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (_hf : 0 < f.degree) : Type

Executable quotient elements, carrying the reducedness invariant in the type.

A value of this type is a polynomial together with a proof that it lies in the image of reduceMod f, so a raw FpPoly p cannot be supplied where one of these is expected.

The modulus is required to be prime, which guarantees the representative is canonical for every nonconstant f: reduceMod is a genuine remainder only when the leading coefficient it divides by is a unit, and over a prime modulus every nonzero coefficient is. Drop the hypothesis and canonicality can fail. At p = 4 with f = 2X the division step subtracts zero and leaves the remainder untouched, so f and 0 are congruent yet both reduced and distinct. isReduced_iff_degree_lt states the contract this hypothesis buys.

Primality is sufficient, not necessary: a monic f needs no coefficient inversion and would be canonical over any modulus. The uniform prime hypothesis is the deliberate choice here, since every modulus this library serves is over a prime field anyway.

reduceMod itself, and its degree-short-circuit lemmas above, stay general; it is the quotient type that is restricted, because that is what carries the canonicality claim.

Equations

• Hex.GFqRing.PolyQuotient f _hf = { g : Hex.FpPoly p // Hex.GFqRing.IsReduced f g }

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

Inject a polynomial into the quotient by reducing it modulo f.

Equations

• Hex.GFqRing.ofPoly f hf g = ⟨Hex.GFqRing.reduceMod f g, ⋯⟩

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

Project a quotient element to its canonical polynomial representative.

Equations

• Hex.GFqRing.repr x = x.val

@[instance_reducible]

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

Quotient elements have decidable equality by comparing their canonical representatives.

Equations

• Hex.GFqRing.instDecidableEqPolyQuotient x y = match decEq x.val y.val with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

@[simp]

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

The canonical representative of ofPoly f hf g is reduceMod f g.

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

Two quotient elements are equal whenever their canonical representatives agree.

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

@[simp]

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

A quotient element equals the canonical zero iff its representative reduces to zero.

@[simp]

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

A quotient element differs from the canonical zero iff its representative reduces nonzero.

@[simp]

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

Canonical representatives have degree strictly below the modulus.

theorem Hex.GFqRing.isReduced_iff_degree_lt {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f : FpPoly p} (hf : 0 < f.degree) (g : FpPoly p) : IsReduced f g ↔ g.degree < f.degree

Reducedness is exactly a degree bound, so the representative a PolyQuotient stores is the unique one of its residue class.

This is the theorem behind the "equality is equality of canonical representatives" contract, and it is where primality is load-bearing. The forward direction is the one that needs it: a reduced polynomial is only known to sit below the modulus because the remainder-degree law holds over a field, and that law is what fails when the leading coefficient of f is not a unit. The converse is reduceMod_eq_self_of_degree_lt, which holds generally.

@[simp]

theorem Hex.GFqRing.reduceMod_idem {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f g : FpPoly p) : reduceMod f (reduceMod f g) = reduceMod f g

Applying reduceMod to a reduced representative is a no-op.

@[simp]

theorem Hex.GFqRing.reduceMod_self {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) : reduceMod f f = 0

The modulus itself reduces to the zero representative modulo itself.

theorem Hex.GFqRing.reduceMod_add_reduceMod_congr {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)

Reducing both summands before quotient reduction preserves the canonical representative.

@[simp]

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

Reducing the left summand before quotient reduction preserves the representative.

@[simp]

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

Reducing the right summand before quotient reduction preserves the representative.

theorem Hex.GFqRing.reduceMod_mul_reduceMod_congr {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)

Reducing both factors before quotient reduction preserves the canonical representative.

@[simp]

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

Reducing the left factor before quotient reduction preserves the representative.

@[simp]

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

Reducing the right factor before quotient reduction preserves the representative.

theorem Hex.GFqRing.reduceMod_add_mul_self_right {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hf : 0 < f.degree) (q r : FpPoly p) : reduceMod f (q + r * f) = reduceMod f q

Adding a right multiple of the modulus does not change the canonical representative.

@[simp]

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

Reducing the argument before applying ofPoly does not change the resulting quotient element.