HexGF2.Field.WordLaws

source

theorem Hex.GF2n.add_comm {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a b : GF2n n irr hn hn64 hirr) :

a + b = b + a

Addition is commutative on the packed single-word field.

source

theorem Hex.GF2n.add_assoc {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a b c : GF2n n irr hn hn64 hirr) :

a + b + c = a + (b + c)

Addition is associative on the packed single-word field.

source

@[simp]

theorem Hex.GF2n.zero_add {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) :

0 + a = a

The additive identity is a left identity.

source

@[simp]

theorem Hex.GF2n.add_zero {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) :

a + 0 = a

The additive identity is a right identity.

source

@[simp]

theorem Hex.GF2n.add_self {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) :

a + a = 0

Every element is its own additive inverse in characteristic two.

source

@[simp]

theorem Hex.GF2n.neg_add_cancel {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) :

-a + a = 0

Negation cancels addition.

source

theorem Hex.GF2n.mul_comm {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a b : GF2n n irr hn hn64 hirr) :

a * b = b * a

Multiplication is commutative on the packed single-word field.

source

theorem Hex.GF2n.mul_assoc {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a b c : GF2n n irr hn hn64 hirr) :

a * b * c = a * (b * c)

Multiplication is associative on the packed single-word field.

source

@[simp]

theorem Hex.GF2n.one_mul {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) :

1 * a = a

The multiplicative identity is a left identity.

source

@[simp]

theorem Hex.GF2n.mul_one {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) :

a * 1 = a

The multiplicative identity is a right identity.

source

@[simp]

theorem Hex.GF2n.zero_mul {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) :

0 * a = 0

Zero annihilates multiplication on the left.

source

@[simp]

theorem Hex.GF2n.mul_zero {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a : GF2n n irr hn hn64 hirr) :

a * 0 = 0

Zero annihilates multiplication on the right.

source

theorem Hex.GF2n.left_distrib {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a b c : GF2n n irr hn hn64 hirr) :

a * (b + c) = a * b + a * c

Multiplication distributes over addition on the left.

source

theorem Hex.GF2n.right_distrib {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} (a b c : GF2n n irr hn hn64 hirr) :

(a + b) * c = a * c + b * c

Multiplication distributes over addition on the right.

source

theorem Hex.GF2n.one_ne_zero {n : Nat} {irr : UInt64} {hn : 0 < n} {hn64 : n < 64} {hirr : (GF2Poly.ofUInt64Monic irr n).Irreducible} :

1 ≠ 0

The packed identity is nonzero for every accepted single-word modulus.