Finite Fields

June 8, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This entry formalizes the classification of the finite fields (also called Galois fields): For each prime power $p^n$ there exists exactly one (up to isomorphisms) finite field of that size and there are no other finite fields. The derivation includes a formalization of the characteristic of rings, the Frobenius endomorphism, formal differentiation for polynomials in HOL-Algebra and Gauss' formula for the number of monic irreducible polynomials over finite fields: $\frac{1}{n} \sum_{d | n} \mu(d) p^{n/d} \textrm{.}$ The proofs are based on the books from Ireland and Rosen, as well as, Lidl and Niederreiter.