Finite Fields

Statement

For every prime $p$ and positive integer $n$, there exists a unique (up to isomorphism) field with exactly $p^n$ elements, denoted $\mathbb{F}_{p^n}$ or $\text{GF}(p,n)$. It is the splitting field of $x^{p^n} - x$ over $\mathbb{F}_p$.

In Mathlib: GaloisField p n is the concrete construction, and GaloisField.card proves Nat.card (GaloisField p n) = p ^ n.

Key structural facts:

• $\mathbb{F}_{p^n}^\times$ is cyclic of order $p^n - 1$.
• $\mathbb{F}_{p^n}$ is Galois over $\mathbb{F}_p$ with cyclic Galois group generated by the Frobenius $\phi: x \mapsto x^p$.
• $\mathbb{F}_{p^m} \subseteq \mathbb{F}_{p^n}$ iff $m \mid n$.

Visualization

The field $\mathbb{F}_4 = \mathbb{F}_2[x]/(x^2+x+1)$.

Elements: $\{0, 1, \alpha, \alpha+1\}$ where $\alpha^2 = \alpha + 1$ (i.e., $\alpha$ is a root of $x^2 + x + 1$).

Addition table (characteristic 2, so $a + a = 0$):

$+$	$0$	$1$	$\alpha$	$\alpha{+}1$
$0$	$0$	$1$	$\alpha$	$\alpha{+}1$
$1$	$1$	$0$	$\alpha{+}1$	$\alpha$
$\alpha$	$\alpha$	$\alpha{+}1$	$0$	$1$
$\alpha{+}1$	$\alpha{+}1$	$\alpha$	$1$	$0$

Multiplication table (using $\alpha^2 = \alpha + 1$):

$\times$	$1$	$\alpha$	$\alpha{+}1$
$1$	$1$	$\alpha$	$\alpha{+}1$
$\alpha$	$\alpha$	$\alpha{+}1$	$1$
$\alpha{+}1$	$\alpha{+}1$	$1$	$\alpha$

Note: $\mathbb{F}_4^\times = \{1, \alpha, \alpha+1\}$ is cyclic of order 3 generated by $\alpha$.

Proof Sketch

1. Existence. The polynomial $x^{p^n} - x$ over $\mathbb{F}_p$ is separable (its derivative is $-1 \ne 0$), so it has $p^n$ distinct roots in its splitting field. These roots form a subfield (closed under addition and multiplication by Freshman's dream), which has exactly $p^n$ elements.
2. Uniqueness. If $F$ is any field with $p^n$ elements, then $F^\times$ has order $p^n - 1$, so every $a \in F^\times$ satisfies $a^{p^n - 1} = 1$, hence $a^{p^n} = a$ for all $a \in F$. Thus $F$ consists exactly of roots of $x^{p^n} - x$, making $F$ the splitting field.
3. Subfield lattice. $\mathbb{F}_{p^m} \subseteq \mathbb{F}_{p^n}$ iff every root of $x^{p^m} - x$ is also a root of $x^{p^n} - x$, which holds iff $p^m - 1 \mid p^n - 1$, iff $m \mid n$.

Connections

Finite fields are the arena for Fermat's Little TheoremFermat's Little Theorem$$a^p \equiv a \pmod{p}$$For prime p, a^p is congruent to a mod pRead more → (the statement $a^p = a$ for $a \in \mathbb{F}_p$ is exactly membership in the splitting field of $x^p - x$). The multiplicative group structure is central to Quadratic ReciprocityQuadratic Reciprocity$$\left(\frac{p}{q}\right)\left(\frac{q}{p}\right) = (-1)^{\frac{p-1}{2}\cdot\frac{q-1}{2}}$$Relationship between solvability of quadratic congruences for two odd primesRead more → via the Legendre symbol over $\mathbb{F}_p$.

/-- The Galois field GF(p, n) has exactly p^n elements. -/
theorem galoisField_card (p : ℕ) [Fact p.Prime] (n : ℕ) (hn : n ≠ 0) :
    Nat.card (GaloisField p n) = p ^ n :=
  GaloisField.card p hn