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

BSD License

### Topics

- Mathematics/Algebra

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

### Depends on

- Dirichlet Series

### Used by

- Universal Hash Families

### Auto-related entries

- Perfect Fields
- Universal Hash Families
- Lehmer’s Theorem

## Cite

×

Finite_Fields-AFP

    @article{Finite_Fields-AFP,
      author  = {Emin Karayel},
      title   = {Finite Fields},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Finite_Fields.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jun 16, 2022 : Isabelle2021-1