@[instance_reducible]

instance HexGF2Mathlib.commRing : CommRing Hex.GF2Poly

The packed F₂[x] representation is a Mathlib commutative ring, with the executable packed operations.

Equations

• HexGF2Mathlib.commRing = CommRing.ofMinimalAxioms Hex.GF2Poly.add_assoc Hex.GF2Poly.zero_add Hex.GF2Poly.neg_add_cancel Hex.GF2Poly.mul_assoc Hex.GF2Poly.mul_comm Hex.GF2Poly.one_mul ⋯

def HexGF2Mathlib.GF2Poly.euclideanRank (p : Hex.GF2Poly) : ℕ

The Euclidean rank of a packed polynomial. Zero has rank zero and a nonzero polynomial has rank one greater than its degree.

Equations

• HexGF2Mathlib.GF2Poly.euclideanRank p = if p = 0 then 0 else p.natDegree + 1

@[simp]

theorem HexGF2Mathlib.GF2Poly.euclideanRank_zero : euclideanRank 0 = 0

@[simp]

theorem HexGF2Mathlib.GF2Poly.euclideanRank_of_ne_zero {p : Hex.GF2Poly} (hp : p ≠ 0) : euclideanRank p = p.natDegree + 1

@[instance_reducible]

instance HexGF2Mathlib.GF2Poly.euclideanDomain : EuclideanDomain Hex.GF2Poly

The packed F₂[x] representation is a Euclidean domain whose quotient and remainder are the executable long-division operations from hex-gf2.

Equations

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

@[instance_reducible]

noncomputable instance HexGF2Mathlib.GF2Poly.gcdMonoid : GCDMonoid Hex.GF2Poly

The gcd-domain interface uses the packed executable gcd, not Mathlib's separate recursive Euclidean-domain implementation.

Equations

• HexGF2Mathlib.GF2Poly.gcdMonoid = gcdMonoidOfGCD Hex.GF2Poly.gcd Hex.GF2Poly.gcd_dvd_left Hex.GF2Poly.gcd_dvd_right ⋯

theorem HexGF2Mathlib.GF2Poly.gcd_eq_packed (p q : Hex.GF2Poly) : gcd p q = p.gcd q

Mathlib's gcd operation on packed polynomials is definitionally the executable hex-gf2 gcd.

theorem HexGF2Mathlib.GF2Poly.euclidean_gcd_eq_packed (p q : Hex.GF2Poly) : EuclideanDomain.gcd p q = p.gcd q

Mathlib's recursive Euclidean gcd agrees with the executable packed gcd. Over F₂[x], mutual divisibility determines equality because 1 is the only unit.

@[instance_reducible]

noncomputable instance HexGF2Mathlib.GF2n.field {n : ℕ} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (Hex.GF2Poly.ofUInt64Monic irr n).Irreducible} : Field (Hex.GF2n n irr hn hn64 hirr)

The packed single-word quotient is a Mathlib field, with its executable core operations retained. Its positive extension degree is part of the type, so unlike GF2nPoly it needs no extra nontriviality hypothesis.

Equations

• HexGF2Mathlib.GF2n.field = Field.ofMinimalAxioms (Hex.GF2n n irr hn hn64 hirr) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance HexGF2Mathlib.GF2nPoly.field {f : Hex.GF2Poly} {hirr : f.Irreducible} [hdeg : Fact (0 < f.natDegree)] : Field (Hex.GF2nPoly f hirr)

The packed quotient is a Mathlib field once the modulus is nonconstant.

The degree hypothesis is not redundant. Hex.GF2Poly.Irreducible asks that f be nonzero with no factorization into two positive-degree parts, which the constant 1 satisfies, and Hex.GF2nPoly 1 _ is the trivial ring where 0 = 1. Carried as a Fact so that instance synthesis can find it: a caller with a genuine modulus supplies it once, and the committed packed entries in hex-gfq carry natDegree_pos to build it from.

Equations

• HexGF2Mathlib.GF2nPoly.field = Field.ofMinimalAxioms (Hex.GF2nPoly f hirr) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯