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, 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.


BSD License


January 18, 2024
Added exectuable algorithms for the construction of (and calculations in) finite fields.
January 17, 2024
Added Rabin's test for the irreducibility of polynomials in finite fields.


Session Finite_Fields