@ARTICLE{FIELD_16.MIZ,
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {Finite Fields},
      ADDRESS1 = {Institute of Informatics, University of Gda{\'n}sk, Poland},
      SECTION1 = {Iteration of Functions},
      SECTION2 = {Induced Subfields},
      SECTION3 = {Some More Preliminaries},
      SECTION4 = {Reduced Rings and Frobenius Morphism},
      SECTION5 = {The Polynomial $X^n - X$},
      SECTION6 = {On Prime Fields of Finite Fields},
      SECTION7 = {Existence and Uniqueness of Finite Fields},
      SECTION8 = {Automorphisms of Finite Fields},
      SECTION9 = {Galois Fields -- as Extensions of $Z/p$},
      DAY = {27},
      MONTH = {December},
      YEAR = {2024},
      SUMMARY = {We continue the formalization of field theory in Mizar.
                 Here we prove existence and uniqueness of finite fields by constructing the
                 splitting field of the polynomial $X^(p^n)-X$ over the prime field of a field
                 with characteristic $p$. We also define the Frobenius morphism and show
                 that the automorphisms of a field with $p^n$ elements are exactly the
                 powers $0, \ldots n-1$ of the Frobenius morphism, that is the automorphism
                 group is generated by the Frobenius morphism.},
      INTRODUCTION = {In this paper we prove existence and uniqueness of finite fields \cite{Lan02,Rad89}
    and also establish the automorphisms of a finite field using the Mizar formalism
    \cite{Mizar-State-2015,BancerekJAR:2018,Kornilowicz:2015:FC,GrabKornSchwarz:2016}.
    \par
    In the first three sections we provide some notation and lemmas needed later.
    First we consider function iterations $f^n$ where $n$ is a natural number.
    We prove some standard properties, amongst others that $f^n$ is an automorphism, if $f$ is.
    Then we deal with subfields: we say that a subset $S$ of a given field $F$ induces a
    subfield of $F$, if $S$ contains $0$ and $1$ and is closed with respect to the field
    operations. It is well known that in this case $S$ with the restricted field operations
    itself is a field; we construct this field by defining a functor InducedSubfield($S$).
    The third section contains a number of technical lemmas, but also the proof that a
    finite extension of a finite field is both again finite and simple.
    \par
    In the fourth section we briefly introduce reduced rings, that is rings in which $0$ is
    the only nilpotent element. Then we define the Frobenius morphism of a ring $R$, which
    is injective, if $R$ is nilpotent$. We also prove that the Frobenious morphism of $Z/p$
    is trivial and that a field $F$ is perfect if and only if its Frobenious morphism
    is bijective.
    \par
    The next section is devoted to the polynomials $X^n-X$. The most important properties
    we prove are that $a$ is a root of $X^n-X$ if and only if $a^n = a$ and that the derivation
    of $X^(p^n)-X$ in a field with characteristic $p$ is $-1$, so that in this case $X^(p^n)-X$
    is separable.
    \par
   Section~6 presents basic properties of prime fields, for example that if $F$ is a field
   with $p^n$ elements, then an element $a$ is in the prime field of $F$ if and only if $a^p = a$.
   The main result is that a finite field with $p^n$ elements is a finite simple extension
   of degree $n$ over its prime field.
   \par
   Section seven is the core of the article, here we show existence and uniqueness of finite fields.
   If $F$ is a field with characteristic $p$, then the splitting field of $X^(p^n)-X$ over $F$'s
   prime field is a field with $p^n$ elements: the roots of $X^(p^n)-X$ induce a field which --
   because $X^(p^n)-X$ is separable -- contains exactly $p^n$ elements. Because two splitting fields
   of $X^(p^n)-X$ are isomorphic, this also implies that two finite fields with the same number of
   elements are isomorphic.
    \par
   In eighth section we prove that the automorphisms of a field $F$ with $p^n$ elements are exactly
    the powers $0, \ldots n-1$ of $F's$ Frobenius morphism. To do so we also showed that in $F(a)$
    where $a$ is algebraic a $F$-fixing automorphism is uniquely determined by $a$, that is from
    $f_1(a) = $f_2(a)$ already follows $f_1 = f_2$. This implies that in this case the set of
   automorphisms is finite.
   \par
    In the last section we define Galois fields over $q$ where $q = p^n$ is a prime power.
   Here we assume that the finite fields contain $Z/p$ as a subfield, so that the prime field
   of a finite field now is $Z/p$. Though this section hence is just a repetition of prior results
   for a special case, we think that in this form the results about finite fields are easier reusable
   in further developments: the results stated as theorems so far, here can be expressed using clusters.}}

@BOOK{Lan02,
      AUTHOR = {Lang, Serge},
      TITLE = {Algebra, {R}evised {T}hird {E}dition},
      PUBLISHER = {Springer Verlag},
      YEAR = {2002}}

@BOOK{Rad89,
      AUTHOR = {Radbruch, Knut},
      TITLE = {Algebra I},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1991}}

@BOOK{Jac85,
      AUTHOR = {Jacobson, Nathan},
      TITLE = {Basic Algebra {I}},
      PUBLISHER = {Dover Books on Mathematics},
      YEAR = {1985}}
