Algebraic Extensions

• Main Authors: Schwarzweller Christoph, Rowińska-Schwarzweller Agnieszka
• Format: Article
• Language: English
• Published: Sciendo 2021-04-01
• Series: Formalized Mathematics
• Subjects: algebraic extensions; finite extensions; field of algebraic numbers; 12f05; 68v20
• Online Access: https://doi.org/10.2478/forma-2021-0004

In this article we further develop field theory in Mizar [1], [2], [3] towards splitting fields. We deal with algebraic extensions [4], [5]: a field extension E of a field F is algebraic, if every element of E is algebraic over F. We prove amongst others that finite extensions are algebraic and that field extensions generated by a finite set of algebraic elements are finite. From this immediately follows that field extensions generated by roots of a polynomial over F are both finite and algebraic. We also define the field of algebraic elements of E over F and show that this field is an intermediate field of E|F.