Algebraic Extensions
Keyword(s):
Summary 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.
Keyword(s):
2001 ◽
Vol 27
(4)
◽
pp. 201-214
◽
1977 ◽
Vol 29
(6)
◽
pp. 1304-1311
◽
Keyword(s):
Keyword(s):