Finite Fields

Emin Karayel 🌐

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.


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


Session Finite_Fields