mathlib documentation

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 #

Main Results #

theorem galois_poly_separable {K : Type u_1} [field K] (p q : ) [char_p K p] (h : p q) :
@[instance]
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
@[instance]
def galois_field.char_p (p : ) [fact (nat.prime p)] (n : ) :
theorem galois_field.finrank (p : ) [fact (nat.prime p)] {n : } (h : n 0) :
theorem galois_field.card (p : ) [fact (nat.prime p)] (n : ) (h : n 0) :

A Galois field with exponent 1 is equivalent to zmod

Equations
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 : fintype.card K = p ^ n) :

Uniqueness of finite fields : Any finite field is isomorphic to some Galois field.

Equations