Finite Fields

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^(pn) −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ⁿ elements are exactly the powers 0, . . ., n − 1 of the Frobenius morphism, that is the automorphism group is generated by the Frobenius morphism.