Introduction to Galois Theory

This article continues a series devoted to the formalization of the Fundamental Theorem of Galois Theory using the Mizar proof assistant. We define groups of automorphisms and fixed fields and establish their fundamental properties. We also introduce an encoding of conjugates for groups of automorphisms and Galois extensions, and present the classical example demonstrating that the field of complex numbers is a Galois extension of the field of real numbers.