# mathlibdocumentation

field_theory.finite.galois_field

# Galois fields #

If p is a prime number, and n a natural number, then galois_field 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 #

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

## Main Results #

• galois_field.alg_equiv_galois_field: Any finite field is isomorphic to some Galois field
• finite_field.alg_equiv_of_card_eq: Uniqueness of finite fields : algebra isomorphism
• finite_field.ring_equiv_of_card_eq: Uniqueness of finite fields : ring isomorphism
theorem galois_poly_separable {K : Type u_1} [field K] (p q : ) [ p] (h : p q) :
@[protected, instance]
noncomputable def galois_field.field (p : ) [fact (nat.prime p)] (n : ) :
def galois_field (p : ) [fact (nat.prime p)] (n : ) :
Type

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

Equations
Instances for galois_field
@[protected, instance]
noncomputable def galois_field.inhabited  :
Equations
@[protected, instance]
noncomputable def galois_field.algebra (p : ) [fact (nat.prime p)] (n : ) :
algebra (zmod p) n)
Equations
@[protected, instance]
def galois_field.char_p (p : ) [fact (nat.prime p)] (n : ) :
char_p n) p
@[protected, instance]
noncomputable def galois_field.fintype (p : ) [fact (nat.prime p)] (n : ) :
Equations
theorem galois_field.finrank (p : ) [fact (nat.prime p)] {n : } (h : n 0) :
n) = n
theorem galois_field.card (p : ) [fact (nat.prime p)] (n : ) (h : n 0) :
noncomputable def galois_field.equiv_zmod_p (p : ) [fact (nat.prime p)] :

A Galois field with exponent 1 is equivalent to zmod

Equations
theorem galois_field.is_splitting_field_of_card_eq (p : ) [fact (nat.prime p)] (n : ) {K : Type u_1} [field K] [fintype K] [algebra (zmod p) K] (h : = p ^ n) :
@[protected, instance]
def galois_field.is_galois {K : Type u_1} {K' : Type u_2} [field K] [field K'] [finite K'] [ K'] :
K'
noncomputable def galois_field.alg_equiv_galois_field (p : ) [fact (nat.prime p)] (n : ) {K : Type u_1} [field K] [fintype K] [algebra (zmod p) K] (h : = p ^ n) :

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

Equations
noncomputable def finite_field.alg_equiv_of_card_eq {K : Type u_1} [field K] [fintype K] {K' : Type u_2} [field K'] [fintype K'] (p : ) [fact (nat.prime p)] [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

Equations
noncomputable def finite_field.ring_equiv_of_card_eq {K : Type u_1} [field K] [fintype K] {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

Equations