Documentation

Mathlib.FieldTheory.Finite.GaloisField

Galois fields #

If p is a prime number, and n a natural number, then GaloisField p n is defined as the splitting field of X^(p^n) - X over ZMod p. It is a finite field with p ^ n elements.

Main definition #

Main Results #

instance FiniteField.isSplittingField_sub (K : Type u_1) (F : Type u_2) [Field K] [Fintype K] [Field F] [Algebra F K] :
Polynomial.IsSplittingField F K (Polynomial.X ^ Fintype.card K - Polynomial.X)
Equations
  • =
theorem galois_poly_separable {K : Type u_1} [Field K] (p : ) (q : ) [CharP K p] (h : p q) :
(Polynomial.X ^ q - Polynomial.X).Separable
def GaloisField (p : ) [Fact (Nat.Prime p)] (n : ) :

A finite field with p ^ n elements. Every field with the same cardinality is (non-canonically) isomorphic to this field.

Equations
Instances For
    instance instFieldGaloisField (p : ) [Fact (Nat.Prime p)] (n : ) :
    Equations
    instance GaloisField.instAlgebraZMod (p : ) [h_prime : Fact (Nat.Prime p)] (n : ) :
    Equations
    instance GaloisField.instIsSplittingFieldZModHSubPolynomialHPowNatX (p : ) [h_prime : Fact (Nat.Prime p)] (n : ) :
    Polynomial.IsSplittingField (ZMod p) (GaloisField p n) (Polynomial.X ^ p ^ n - Polynomial.X)
    Equations
    • =
    instance GaloisField.instCharP (p : ) [h_prime : Fact (Nat.Prime p)] (n : ) :
    Equations
    • =
    Equations
    • =
    theorem GaloisField.finrank (p : ) [h_prime : Fact (Nat.Prime p)] {n : } (h : n 0) :
    theorem GaloisField.card (p : ) [h_prime : Fact (Nat.Prime p)] (n : ) (h : n 0) :
    theorem GaloisField.splits_zmod_X_pow_sub_X (p : ) [h_prime : Fact (Nat.Prime p)] :
    Polynomial.Splits (RingHom.id (ZMod p)) (Polynomial.X ^ p - Polynomial.X)

    A Galois field with exponent 1 is equivalent to ZMod

    Equations
    Instances For
      theorem GaloisField.splits_X_pow_card_sub_X (p : ) [h_prime : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod p) K] :
      Polynomial.Splits (algebraMap (ZMod p) K) (Polynomial.X ^ Fintype.card K - Polynomial.X)
      theorem GaloisField.isSplittingField_of_card_eq (p : ) [h_prime : Fact (Nat.Prime p)] (n : ) {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod p) K] (h : Fintype.card K = p ^ n) :
      Polynomial.IsSplittingField (ZMod p) K (Polynomial.X ^ p ^ n - Polynomial.X)
      @[instance 100]
      instance GaloisField.instIsGaloisOfFinite {K : Type u_2} {K' : Type u_3} [Field K] [Field K'] [Finite K'] [Algebra K K'] :
      Equations
      • =
      def GaloisField.algEquivGaloisField (p : ) [h_prime : Fact (Nat.Prime p)] (n : ) {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod p) K] (h : Fintype.card K = p ^ n) :

      Any finite field is (possibly non canonically) isomorphic to some Galois field.

      Equations
      Instances For
        def FiniteField.algEquivOfCardEq {K : Type u_1} [Field K] [Fintype K] {K' : Type u_2} [Field K'] [Fintype K'] (p : ) [h_prime : Fact (Nat.Prime p)] [Algebra (ZMod p) K] [Algebra (ZMod p) K'] (hKK' : Fintype.card K = Fintype.card K') :

        Uniqueness of finite fields: Any two finite fields of the same cardinality are (possibly non canonically) isomorphic

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def FiniteField.ringEquivOfCardEq {K : Type u_1} [Field K] [Fintype K] {K' : Type u_2} [Field K'] [Fintype K'] (hKK' : Fintype.card K = Fintype.card K') :
          K ≃+* K'

          Uniqueness of finite fields: Any two finite fields of the same cardinality are (possibly non canonically) isomorphic

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