# 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 #

• GaloisField p n is a field with p ^ n elements

## Main Results #

• GaloisField.algEquivGaloisField: Any finite field is isomorphic to some Galois field
• FiniteField.algEquivOfCardEq: Uniqueness of finite fields : algebra isomorphism
• FiniteField.ringEquivOfCardEq: Uniqueness of finite fields : ring isomorphism
instance FiniteField.isSplittingField_sub (K : Type u_1) (F : Type u_2) [] [] [] [Algebra F K] :
Polynomial.IsSplittingField F K (Polynomial.X ^ - Polynomial.X)
theorem galois_poly_separable {K : Type u_1} [] (p : ) (q : ) [CharP K p] (h : p q) :
Polynomial.Separable (Polynomial.X ^ q - Polynomial.X)
def GaloisField (p : ) [Fact ()] (n : ) :

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

Instances For
instance instFieldGaloisField (p : ) [Fact ()] (n : ) :
instance GaloisField.instFintypeGaloisField (p : ) [h_prime : Fact ()] (n : ) :
theorem GaloisField.finrank (p : ) [h_prime : Fact ()] {n : } (h : n 0) :
theorem GaloisField.card (p : ) [h_prime : Fact ()] (n : ) (h : n 0) :
theorem GaloisField.splits_zmod_X_pow_sub_X (p : ) [h_prime : Fact ()] :
Polynomial.Splits (RingHom.id (ZMod p)) (Polynomial.X ^ p - Polynomial.X)
def GaloisField.equivZmodP (p : ) [h_prime : Fact ()] :

A Galois field with exponent 1 is equivalent to ZMod

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

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

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

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

Instances For
def FiniteField.ringEquivOfCardEq {K : Type u_1} [] [] {K' : Type u_2} [Field K'] [Fintype K'] (hKK' : ) :
K ≃+* K'

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

Instances For