The Lattice of Intermediate Fields and Other Preliminaries to Galois Theory

This article initiates a series devoted to the formalization of the Fundamental Theorem of Galois Theory. It presents several preliminaries required for the formal development of Galois theory. In particular, as a main result, we define the lattice of intermediate fields of an extension E/F; we also treat sets of functions, groups, and intermediate fields in order to provide the necessary cluster registrations that enable effective Mizar automation.