theorem Hex.GF2nPoly.eq_of_val_eq {f : GF2Poly} {hirr : f.Irreducible} {a b : GF2nPoly f hirr} (h : a.val = b.val) : a = b

Equality of packed polynomial representatives follows from equality of their stored reduced polynomials.

@[instance_reducible]

instance Hex.GF2nPoly.instDecidableEq {f : GF2Poly} {hirr : f.Irreducible} : DecidableEq (GF2nPoly f hirr)

Decidable equality on the quotient field GF2nPoly f hirr, decided on the underlying reduced representative .val; representatives with equal .val are promoted to equal field elements via eq_of_val_eq.

Equations

• a.instDecidableEq b = match decEq a.val b.val with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

def Hex.GF2nPoly.coeffVector {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : Fin f.natDegree → Bool

Finite-index coefficient code for the reduced representative of a packed quotient-field element.

Equations

• a.coeffVector = Hex.GF2Poly.reducedCoeffVector f.natDegree a.val

theorem Hex.GF2nPoly.eq_of_coeffVector_eq {f : GF2Poly} {hirr : f.Irreducible} {a b : GF2nPoly f hirr} (hcoeff : a.coeffVector = b.coeffVector) : a = b

The coefficient code is injective on packed quotient-field elements.

def Hex.GF2nPoly.modulus {f : GF2Poly} : GF2Poly

The defining irreducible modulus polynomial of the packed quotient field.

Equations

• Hex.GF2nPoly.modulus = f

theorem Hex.GF2nPoly.zero_reduced {f : GF2Poly} : GF2Poly.IsZero 0 ∨ GF2Poly.natDegree 0 < f.natDegree

Zero is a reduced representative modulo any packed irreducible.

def Hex.GF2nPoly.reducePoly {f : GF2Poly} {hirr : f.Irreducible} (p : GF2Poly) : GF2nPoly f hirr

Reduce a packed polynomial to its canonical residue class modulo f.

Equations

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

@[simp]

theorem Hex.GF2nPoly.reducePoly_val_eq_mod {f : GF2Poly} {hirr : f.Irreducible} (p : GF2Poly) : (reducePoly p).val = p % f

The value stored by canonical quotient reduction is the ordinary remainder modulo the irreducible modulus.

theorem Hex.GF2nPoly.reducePoly_eq_iff_mod_eq {f : GF2Poly} {hirr : f.Irreducible} {p q : GF2Poly} : reducePoly p = reducePoly q ↔ p % f = q % f

Two raw polynomials pack to the same quotient representative exactly when they agree modulo f; the reduction map is injective up to f-residue.

theorem Hex.GF2nPoly.reducePoly_mod_eq {f : GF2Poly} {hirr : f.Irreducible} (p : GF2Poly) : reducePoly (p % f) = reducePoly p

Reducing an already-computed remainder gives the same quotient class as reducing the original polynomial.

theorem Hex.GF2nPoly.mod_mul_mod_eq_mod_mul (p q f : GF2Poly) : p % f * (q % f) % f = p * q % f

Reduction % f commutes with multiplication: reducing the product of two remainders gives the same result as reducing the product directly. This makes multiplication on the quotient GF2nPoly f hirr well-defined on reduced representatives.

def Hex.GF2nPoly.zero {f : GF2Poly} {hirr : f.Irreducible} : GF2nPoly f hirr

Canonical additive identity.

Equations

• Hex.GF2nPoly.zero = { val := 0, val_reduced := ⋯ }

@[instance_reducible]

instance Hex.GF2nPoly.instZero {f : GF2Poly} {hirr : f.Irreducible} : Zero (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instZero = { zero := Hex.GF2nPoly.zero }

@[simp]

theorem Hex.GF2nPoly.reducePoly_zero {f : GF2Poly} {hirr : f.Irreducible} : reducePoly 0 = 0

Reducing the zero polynomial gives the quotient zero.

theorem Hex.GF2nPoly.reducePoly_eq_zero_iff_dvd {f : GF2Poly} {hirr : f.Irreducible} {p : GF2Poly} (hf : f ≠ 0) : reducePoly p = 0 ↔ f ∣ p

A polynomial reduces to the zero quotient element exactly when the modulus divides it in GF(2)[X].

theorem Hex.GF2nPoly.nodup_map_of_injective {α β : Type} {xs : List α} {g : α → β} (hxs : xs.Nodup) (hinj : ∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → g a = g b → a = b) : (List.map g xs).Nodup

A list map is duplicate-free when the map is injective on the list's own members. Weaker than global injectivity, which is what the element enumerations need: multiplication by a fixed nonzero quotient element is injective on the nonzero elements without being injective on all of them.

theorem Hex.GF2nPoly.length_filter_ne_eq_pred_of_mem_nodup {α : Type} [DecidableEq α] {z : α} {xs : List α} : z ∈ xs → xs.Nodup → (List.filter (fun (a : α) => decide (a ≠ z)) xs).length = xs.length - 1

Deleting a member of a duplicate-free list by filtering shortens it by exactly one. The Nodup hypothesis is what rules out the filter removing several copies at once.

def Hex.GF2nPoly.boolListExpression {f : GF2Poly} {hirr : f.Irreducible} (bs : List Bool) : GF2nPoly f hirr

Evaluate a Boolean coefficient list as a quotient expression in the class of X. The list is low-coefficient first: bs[i] is the coefficient of X^i.

Equations

• Hex.GF2nPoly.boolListExpression bs = Hex.GF2nPoly.reducePoly (Hex.GF2Poly.Internal.ofBoolList bs)

theorem Hex.GF2nPoly.boolListExpression_val_eq_mod {f : GF2Poly} {hirr : f.Irreducible} (bs : List Bool) : (boolListExpression bs).val = GF2Poly.Internal.ofBoolList bs % f

The value of a Boolean quotient expression is the reduced packed polynomial built from the same coefficient list.

def Hex.GF2nPoly.elements {f : GF2Poly} {hirr : f.Irreducible} : List (GF2nPoly f hirr)

Public quotient-field enumeration: all packed representatives in GF2[X]/(f), obtained by reducing every length-f.natDegree Boolean coefficient list. This is exposed for finite-field cardinality, root-count, and Rabin soundness consumers.

Equations

• Hex.GF2nPoly.elements = List.map Hex.GF2nPoly.boolListExpression (Hex.GF2Poly.Internal.coeffBoolLists f.natDegree)

@[simp]

theorem Hex.GF2nPoly.elements_length {f : GF2Poly} {hirr : f.Irreducible} : elements.length = 2 ^ f.natDegree

The quotient field GF2[X]/(f) has exactly 2 ^ f.natDegree elements, the expected cardinality of a degree-f.natDegree extension of GF(2).

theorem Hex.GF2nPoly.mem_elements {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : a ∈ elements

Every packed quotient-field element appears in elements.

theorem Hex.GF2nPoly.boolListExpression_coeffVector {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : boolListExpression (List.ofFn a.coeffVector) = a

The quotient expression built from an element's coefficient vector is that element.

theorem Hex.GF2nPoly.exists_boolListExpression {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : ∃ (bs : List Bool), bs.length = f.natDegree ∧ boolListExpression bs = a

Every packed quotient element is generated by a Boolean coefficient list in the class of X, with exactly f.natDegree coefficients.

theorem Hex.GF2nPoly.elements_nodup {f : GF2Poly} {hirr : f.Irreducible} : elements.Nodup

The quotient enumeration has no duplicate elements.

theorem Hex.GF2nPoly.elements_card {f : GF2Poly} {hirr : f.Irreducible} : elements.length = 2 ^ f.natDegree

The quotient has 2 ^ f.natDegree canonical representatives.

def Hex.GF2nPoly.nonzeroElements {f : GF2Poly} {hirr : f.Irreducible} : List (GF2nPoly f hirr)

The nonzero packed quotient-field elements, as a duplicate-free sublist of elements.

Equations

• Hex.GF2nPoly.nonzeroElements = List.filter (fun (a : Hex.GF2nPoly f hirr) => decide (a ≠ 0)) Hex.GF2nPoly.elements

theorem Hex.GF2nPoly.mem_nonzeroElements {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : a ∈ nonzeroElements ↔ a ≠ 0

Membership in nonzeroElements is exactly nonzero quotient membership.

theorem Hex.GF2nPoly.nonzeroElements_nodup {f : GF2Poly} {hirr : f.Irreducible} : nonzeroElements.Nodup

The nonzero quotient enumeration has no duplicates.

theorem Hex.GF2nPoly.nonzeroElements_card {f : GF2Poly} {hirr : f.Irreducible} : nonzeroElements.length = 2 ^ f.natDegree - 1

There are 2 ^ f.natDegree - 1 nonzero quotient representatives.

def Hex.GF2nPoly.X {f : GF2Poly} {hirr : f.Irreducible} : GF2nPoly f hirr

The quotient class of X modulo the packed irreducible f.

Equations

• Hex.GF2nPoly.X = Hex.GF2nPoly.reducePoly (Hex.GF2Poly.monomial 1)

def Hex.GF2nPoly.one {f : GF2Poly} {hirr : f.Irreducible} : GF2nPoly f hirr

Canonical multiplicative identity.

Equations

• Hex.GF2nPoly.one = Hex.GF2nPoly.reducePoly 1

@[instance_reducible]

instance Hex.GF2nPoly.instOne {f : GF2Poly} {hirr : f.Irreducible} : One (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instOne = { one := Hex.GF2nPoly.one }

def Hex.GF2nPoly.natCast {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) : GF2nPoly f hirr

Natural-number literals reduce to parity in characteristic two.

Equations

• Hex.GF2nPoly.natCast k = if k % 2 = 0 then Hex.GF2nPoly.zero else Hex.GF2nPoly.one

@[instance_reducible]

instance Hex.GF2nPoly.instNatCast {f : GF2Poly} {hirr : f.Irreducible} : NatCast (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instNatCast = { natCast := Hex.GF2nPoly.natCast }

@[instance_reducible]

instance Hex.GF2nPoly.instOfNat {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) : OfNat (GF2nPoly f hirr) k

Equations

• Hex.GF2nPoly.instOfNat k = { ofNat := Hex.GF2nPoly.natCast k }

def Hex.GF2nPoly.add {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : GF2nPoly f hirr

Addition in characteristic two is XOR on representatives, followed by canonical reduction modulo f.

Equations

• a.add b = Hex.GF2nPoly.reducePoly (a.val + b.val)

@[instance_reducible]

instance Hex.GF2nPoly.instAdd {f : GF2Poly} {hirr : f.Irreducible} : Add (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instAdd = { add := Hex.GF2nPoly.add }

theorem Hex.GF2nPoly.reducePoly_add_eq {f : GF2Poly} {hirr : f.Irreducible} (p q : GF2Poly) : reducePoly (p + q) = reducePoly ((reducePoly p).val + (reducePoly q).val)

Reducing a polynomial sum agrees with adding the reduced quotient representatives.

def Hex.GF2nPoly.neg {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : GF2nPoly f hirr

Negation is the identity in characteristic two.

Equations

• a.neg = a

@[instance_reducible]

instance Hex.GF2nPoly.instNeg {f : GF2Poly} {hirr : f.Irreducible} : Neg (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instNeg = { neg := Hex.GF2nPoly.neg }

def Hex.GF2nPoly.sub {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : GF2nPoly f hirr

Subtraction coincides with addition in characteristic two.

Equations

• a.sub b = a.add b

@[instance_reducible]

instance Hex.GF2nPoly.instSub {f : GF2Poly} {hirr : f.Irreducible} : Sub (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instSub = { sub := Hex.GF2nPoly.sub }

def Hex.GF2nPoly.nsmul {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) (a : GF2nPoly f hirr) : GF2nPoly f hirr

Natural scalar multiplication depends only on parity.

Equations

• Hex.GF2nPoly.nsmul k a = if k % 2 = 0 then 0 else a

@[instance_reducible]

instance Hex.GF2nPoly.instSMulNat {f : GF2Poly} {hirr : f.Irreducible} : SMul Nat (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instSMulNat = { smul := Hex.GF2nPoly.nsmul }

def Hex.GF2nPoly.mul {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : GF2nPoly f hirr

Multiplication uses packed GF2Poly multiplication followed by reduction modulo the irreducible defining polynomial.

Equations

• a.mul b = Hex.GF2nPoly.reducePoly (a.val * b.val)

@[instance_reducible]

instance Hex.GF2nPoly.instMul {f : GF2Poly} {hirr : f.Irreducible} : Mul (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instMul = { mul := Hex.GF2nPoly.mul }

theorem Hex.GF2nPoly.reducePoly_mul_eq {f : GF2Poly} {hirr : f.Irreducible} (p q : GF2Poly) : reducePoly (p * q) = reducePoly ((reducePoly p).val * (reducePoly q).val)

Reducing a polynomial product agrees with multiplying the reduced quotient representatives.

def Hex.GF2nPoly.pow {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (k : Nat) : GF2nPoly f hirr

Natural power in the packed quotient field by repeated squaring.

Equations

• a.pow k = Hex.GF2nPoly.pow.go 1 a k

@[irreducible]

def Hex.GF2nPoly.pow.go {f : GF2Poly} {hirr : f.Irreducible} (acc base : GF2nPoly f hirr) (k : Nat) : GF2nPoly f hirr

Square-and-multiply accumulator loop for GF2nPoly.pow: go acc base k computes acc * base ^ k.

Equations

• Hex.GF2nPoly.pow.go acc base k = if hk : k = 0 then acc else have acc' := if k % 2 = 1 then acc * base else acc; have base' := base * base; Hex.GF2nPoly.pow.go acc' base' (k / 2)

@[instance_reducible]

instance Hex.GF2nPoly.instPowNat {f : GF2Poly} {hirr : f.Irreducible} : Pow (GF2nPoly f hirr) Nat

Equations

• Hex.GF2nPoly.instPowNat = { pow := Hex.GF2nPoly.pow }

def Hex.GF2nPoly.frobeniusIter {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : Nat → GF2nPoly f hirr

Iterated Frobenius squaring in the packed quotient, starting from a specified quotient element.

Equations

• a.frobeniusIter 0 = a
• a.frobeniusIter k.succ = a.frobeniusIter k * a.frobeniusIter k

@[simp]

theorem Hex.GF2nPoly.frobeniusIter_zero {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : a.frobeniusIter 0 = a

Zero Frobenius iterations leave the quotient element unchanged.

@[simp]

theorem Hex.GF2nPoly.frobeniusIter_succ {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (k : Nat) : a.frobeniusIter (k + 1) = a.frobeniusIter k * a.frobeniusIter k

One more Frobenius iteration squares the previous iterate in the quotient field.

theorem Hex.GF2nPoly.frobeniusIter_add {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (m n : Nat) : (a.frobeniusIter m).frobeniusIter n = a.frobeniusIter (m + n)

Frobenius iterates compose by adding their iteration counts.

theorem Hex.GF2nPoly.quotient_X_frobeniusIter_eq_reduce_xpow2kMod {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) : X.frobeniusIter k = reducePoly (f.xpow2kMod k)

Iterated quotient squaring of the class of X follows the executable xpow2kMod remainder chain used by Rabin soundness.

def Hex.GF2nPoly.intCast {f : GF2Poly} {hirr : f.Irreducible} (k : Int) : GF2nPoly f hirr

Integer literals reduce to parity.

Equations

• Hex.GF2nPoly.intCast k = Hex.GF2nPoly.natCast k.natAbs

@[instance_reducible]

instance Hex.GF2nPoly.instIntCast {f : GF2Poly} {hirr : f.Irreducible} : IntCast (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instIntCast = { intCast := Hex.GF2nPoly.intCast }

def Hex.GF2nPoly.zsmul {f : GF2Poly} {hirr : f.Irreducible} (k : Int) (a : GF2nPoly f hirr) : GF2nPoly f hirr

Integer scalar multiplication depends only on parity.

Equations

• Hex.GF2nPoly.zsmul k a = if k.natAbs % 2 = 0 then 0 else a

@[instance_reducible]

instance Hex.GF2nPoly.instSMulInt {f : GF2Poly} {hirr : f.Irreducible} : SMul Int (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instSMulInt = { smul := Hex.GF2nPoly.zsmul }

def Hex.GF2nPoly.invPoly {f : GF2Poly} (p : GF2Poly) : GF2Poly

The extended Euclidean witness supplies an inverse candidate modulo the packed irreducible.

Equations

• Hex.GF2nPoly.invPoly p = (p.xgcd Hex.GF2nPoly.modulus).left

def Hex.GF2nPoly.inv {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : GF2nPoly f hirr

Inversion follows the packed extended-GCD path and uses the usual junk value 0⁻¹ = 0.

Equations

• a.inv = if a.val.isZero = true then 0 else Hex.GF2nPoly.reducePoly (Hex.GF2nPoly.invPoly a.val)

@[instance_reducible]

instance Hex.GF2nPoly.instInv {f : GF2Poly} {hirr : f.Irreducible} : Inv (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instInv = { inv := Hex.GF2nPoly.inv }

def Hex.GF2nPoly.div {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : GF2nPoly f hirr

Division is multiplication by the inverse candidate.

Equations

• a.div b = a * b⁻¹

@[instance_reducible]

instance Hex.GF2nPoly.instDiv {f : GF2Poly} {hirr : f.Irreducible} : Div (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instDiv = { div := Hex.GF2nPoly.div }

def Hex.GF2nPoly.zpow {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : Int → GF2nPoly f hirr

Integer exponentiation uses inversion for negative exponents.

Equations

• a.zpow (Int.ofNat k) = a ^ k
• a.zpow (Int.negSucc k) = (a ^ (k + 1))⁻¹

@[instance_reducible]

instance Hex.GF2nPoly.instHPowInt {f : GF2Poly} {hirr : f.Irreducible} : HPow (GF2nPoly f hirr) Int (GF2nPoly f hirr)

Equations

• Hex.GF2nPoly.instHPowInt = { hPow := Hex.GF2nPoly.zpow }

theorem Hex.GF2nPoly.div_eq_mul_inv {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : a / b = a * b⁻¹

Division in GF2nPoly unfolds to multiplication by the multiplicative inverse.

@[simp]

theorem Hex.GF2nPoly.inv_zero {f : GF2Poly} {hirr : f.Irreducible} : 0⁻¹ = 0

The inverse of 0 in GF2nPoly is 0 (the field convention that makes inversion total).

theorem Hex.GF2nPoly.mul_inv_cancel {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (ha : a ≠ 0) : a * a⁻¹ = 1

Every nonzero element of GF2nPoly cancels against its inverse, witnessing that GF2nPoly is a field.

@[simp]

theorem Hex.GF2nPoly.mul_val {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : (a * b).val = a.val * b.val % f

The value of a quotient product is the polynomial product reduced modulo the defining irreducible.

@[simp]

theorem Hex.GF2nPoly.one_val {f : GF2Poly} {hirr : f.Irreducible} : val 1 = 1 % f

The value of the multiplicative identity is (1 : GF2Poly) % f.

@[simp]

theorem Hex.GF2nPoly.add_val {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : (a + b).val = (a.val + b.val) % f

The value of a quotient sum is the polynomial sum reduced modulo the defining irreducible.

@[simp]

theorem Hex.GF2nPoly.neg_val {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : (-a).val = a.val

Negation is the identity on the packed quotient.

@[simp]

theorem Hex.GF2nPoly.sub_val {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : (a - b).val = (a.val + b.val) % f

Subtraction coincides with addition on the packed quotient.

@[simp]

theorem Hex.GF2nPoly.zero_val {f : GF2Poly} {hirr : f.Irreducible} : val 0 = 0

The value of the additive identity is the zero polynomial.

theorem Hex.GF2nPoly.val_mod_eq {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : a.val % f = a.val

A reduced quotient value is its own remainder modulo f.

theorem Hex.GF2nPoly.add_comm {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : a + b = b + a

Addition is commutative on the packed quotient.

theorem Hex.GF2nPoly.add_assoc {f : GF2Poly} {hirr : f.Irreducible} (a b c : GF2nPoly f hirr) : a + b + c = a + (b + c)

Addition is associative on the packed quotient.

theorem Hex.GF2nPoly.add_pair_swap_quot {f : GF2Poly} {hirr : f.Irreducible} (a b c d : GF2nPoly f hirr) : a + b + (c + d) = a + c + (b + d)

Regroup a sum of two pairs by swapping the inner terms. Commutativity and associativity give this, but as a single rewrite it keeps the characteristic-two cancellation arguments from turning into long rw chains.

@[simp]

theorem Hex.GF2nPoly.zero_add {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : 0 + a = a

The additive identity is a left identity.

@[simp]

theorem Hex.GF2nPoly.add_zero {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : a + 0 = a

The additive identity is a right identity.

@[simp]

theorem Hex.GF2nPoly.add_self {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : a + a = 0

Every packed quotient element is its own additive inverse in characteristic two.

@[simp]

theorem Hex.GF2nPoly.mul_zero {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : a * 0 = 0

Multiplication by zero on the right is zero.

@[simp]

theorem Hex.GF2nPoly.zero_mul {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : 0 * a = 0

Multiplication by zero on the left is zero.

theorem Hex.GF2nPoly.mul_comm {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : a * b = b * a

Multiplication is commutative on the packed quotient.

theorem Hex.GF2nPoly.mul_assoc {f : GF2Poly} {hirr : f.Irreducible} (a b c : GF2nPoly f hirr) : a * b * c = a * (b * c)

Multiplication is associative on the packed quotient.

@[simp]

theorem Hex.GF2nPoly.one_mul {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : 1 * a = a

The multiplicative identity is a left identity.

@[simp]

theorem Hex.GF2nPoly.mul_one {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) : a * 1 = a

The multiplicative identity is a right identity.

theorem Hex.GF2nPoly.left_distrib {f : GF2Poly} {hirr : f.Irreducible} (a b c : GF2nPoly f hirr) : a * (b + c) = a * b + a * c

Multiplication distributes over addition on the left in the packed quotient.

theorem Hex.GF2nPoly.right_distrib {f : GF2Poly} {hirr : f.Irreducible} (a b c : GF2nPoly f hirr) : (a + b) * c = a * c + b * c

Multiplication distributes over addition on the right in the packed quotient.

theorem Hex.GF2nPoly.add_sq {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) : (a + b) * (a + b) = a * a + b * b

Squaring a sum is additive in characteristic two.

theorem Hex.GF2nPoly.one_ne_zero {f : GF2Poly} {hirr : f.Irreducible} (hf_pos : 0 < f.natDegree) : 1 ≠ 0

The quotient identity is not zero under a positive-degree modulus.