Documentation

HexGF2.Field.Grind

source
@[simp]
theorem Hex.GF2nPoly.natCast_succ {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) :
natCast (k + 1) = natCast k + 1

Natural literals step by one, which in characteristic two alternates.

source
@[simp]
theorem Hex.GF2nPoly.nsmul_eq_natCast_mul {f : GF2Poly} {hirr : f.Irreducible} (k : Nat) (a : GF2nPoly f hirr) :
k • a = natCast k * a

Scalar multiplication by a natural is multiplication by its cast, since both depend only on parity.

source
@[simp]
theorem Hex.GF2nPoly.pow_zero {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) :
a ^ 0 = 1

The zeroth power is one, through the linear reference.

source
@[simp]
theorem Hex.GF2nPoly.pow_succ {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (n : Nat) :
a ^ (n + 1) = a ^ n * a

Each successor power multiplies by one more factor, through the linear reference: the executable power is square-and-multiply, so this is not definitional.

source
@[simp]
theorem Hex.GF2nPoly.neg_eq_self {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) :
-a = a

Negation is the identity in characteristic two.

source
@[simp]
theorem Hex.GF2nPoly.neg_add_cancel {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) :
-a + a = 0

Additive inverses cancel, which in characteristic two is add_self.

source
@[simp]
theorem Hex.GF2nPoly.sub_eq_add_neg {f : GF2Poly} {hirr : f.Irreducible} (a b : GF2nPoly f hirr) :
a - b = a + -b

Subtraction is addition of the negation, which here is addition.

source
@[instance_reducible]
instance Hex.GF2nPoly.instSemiring {f : GF2Poly} {hirr : f.Irreducible} :
Lean.Grind.Semiring (GF2nPoly f hirr)

Additive and multiplicative structure for the packed quotient field.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem Hex.GF2nPoly.neg_zsmul {f : GF2Poly} {hirr : f.Irreducible} (i : Int) (a : GF2nPoly f hirr) :
-i • a = -(i • a)

Integer scalar multiplication negates with its scalar, which in characteristic two is trivial on both sides.

source
theorem Hex.GF2nPoly.intCast_neg {f : GF2Poly} {hirr : f.Irreducible} (i : Int) :
↑(-i) = -↑i

Integer casts negate trivially, since negation is the identity.

source
@[instance_reducible]
instance Hex.GF2nPoly.instRing {f : GF2Poly} {hirr : f.Irreducible} :
Lean.Grind.Ring (GF2nPoly f hirr)

Additive inverses for the packed quotient.

Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
instance Hex.GF2nPoly.instCommRing {f : GF2Poly} {hirr : f.Irreducible} :
Lean.Grind.CommRing (GF2nPoly f hirr)

Multiplication is commutative, inherited from the packed polynomial ring.

Equations
source
@[simp]
theorem Hex.GF2nPoly.zpow_zero {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) :
a ^ 0 = 1

The zeroth integer power is one.

source
theorem Hex.GF2nPoly.zpow_succ {f : GF2Poly} {hirr : f.Irreducible} (a : GF2nPoly f hirr) (n : Nat) :
a ^ (↑n + 1) = a ^ ↑n * a

Successor integer powers multiply by one more factor.

source
theorem Hex.GF2nPoly.zero_ne_one_of_degree_pos {f : GF2Poly} {hirr : f.Irreducible} (hdeg : 0 < f.natDegree) :
0 ≠ 1

Zero and one are distinct when the modulus is nonconstant.

source
theorem Hex.GF2nPoly.inv_one_of_degree_pos {f : GF2Poly} {hirr : f.Irreducible} (hdeg : 0 < f.natDegree) :
1⁻¹ = 1

One is its own inverse.

source
theorem Hex.GF2nPoly.inv_ne_zero_of_degree_pos {f : GF2Poly} {hirr : f.Irreducible} (hdeg : 0 < f.natDegree) {a : GF2nPoly f hirr} (ha : a ≠ 0) :
a⁻¹ ≠ 0

A nonzero element has a nonzero inverse.

source
theorem Hex.GF2nPoly.inv_inv_of_degree_pos {f : GF2Poly} {hirr : f.Irreducible} (hdeg : 0 < f.natDegree) (a : GF2nPoly f hirr) :
a⁻¹⁻¹ = a

Inversion is an involution, by cancelling through the defining identity.

source
theorem Hex.GF2nPoly.zpow_neg_of_degree_pos {f : GF2Poly} {hirr : f.Irreducible} (hdeg : 0 < f.natDegree) (a : GF2nPoly f hirr) (n : Int) :
a ^ (-n) = (a ^ n)⁻¹

Negating an integer exponent inverts the power.

source
@[instance_reducible]
def Hex.GF2nPoly.fieldOfDegreePos {f : GF2Poly} {hirr : f.Irreducible} (hdeg : 0 < f.natDegree) :
Lean.Grind.Field (GF2nPoly f hirr)

Field laws for the packed quotient, given a nonconstant irreducible modulus.

Not an instance: see the note above on why irreducibility alone is not enough.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Hex.GF2nPoly.isCharPOfDegreePos {f : GF2Poly} {hirr : f.Irreducible} (hdeg : 0 < f.natDegree) :
    Lean.Grind.IsCharP (GF2nPoly f hirr) 2

    Characteristic two, given a nonconstant irreducible modulus.