mathlib3 documentation

field_theory.finite.galois_field

Galois fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
@[protected, instance]
noncomputable def galois_field.field (p : ) [fact (nat.prime p)] (n : ) :
def galois_field (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 galois_field
@[protected, instance]
noncomputable def galois_field.inhabited  :
Equations
@[protected, instance]
noncomputable def galois_field.algebra (p : ) [fact (nat.prime p)] (n : ) :
Equations
@[protected, instance]
def galois_field.char_p (p : ) [fact (nat.prime p)] (n : ) :
@[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) :
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
@[protected, instance]
def galois_field.is_galois {K : Type u_1} {K' : Type u_2} [field K] [field K'] [finite K'] [algebra 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 : fintype.card K = 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' : fintype.card K = fintype.card K') :

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' : 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