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