Finite Fields

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, Rabin's test for the irreducibility of polynomials 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 and publications from Ireland and Rosen, Rabin, as well as, Lidl and Niederreiter.