Normal field extensions
In this file we define normal field extensions and prove that for a finite extension, being normal is the same as being a splitting field (TODO).
Main Definitions
normal F KwhereKis a field extension ofF.
@[class]
Typeclass for normal field extension: K is a normal extension of F iff the minimal
polynomial of every element x in K splits in K, i.e. every conjugate of x is in K.
Equations
- normal F K = ∀ (x : K), ∃ (H : is_integral F x), polynomial.splits (algebra_map F K) (minimal_polynomial H)
Instances
theorem
normal.is_integral
(F : Type u)
(K : Type v)
[field F]
[field K]
[algebra F K]
[h : normal F K]
(x : K) :
is_integral F x
theorem
normal.splits
(F : Type u)
(K : Type v)
[field F]
[field K]
[algebra F K]
[h : normal F K]
(x : K) :
polynomial.splits (algebra_map F K) (minimal_polynomial _)
theorem
normal.exists_is_splitting_field
(F : Type u)
(K : Type v)
[field F]
[field K]
[algebra F K]
[normal F K]
[finite_dimensional F K] :
∃ (p : polynomial F), polynomial.is_splitting_field F K p