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

### License

### History

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

### Topics

### Session Finite_Fields

- Finite_Fields_Preliminary_Results
- Finite_Fields_Factorization_Ext
- Ring_Characteristic
- Formal_Polynomial_Derivatives
- Monic_Polynomial_Factorization
- Card_Irreducible_Polynomials_Aux
- Card_Irreducible_Polynomials
- Finite_Fields_Isomorphic
- Rabin_Irreducibility_Test
- Finite_Fields_Indexed_Algebra_Code
- Finite_Fields_Poly_Ring_Code
- Finite_Fields_Mod_Ring_Code
- Rabin_Irreducibility_Test_Code
- Finite_Fields_More_Bijections
- Finite_Fields_More_PMF
- Finite_Fields_Poly_Factor_Ring_Code
- Find_Irreducible_Poly