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.
BSD License