English
For any finite-dimensional IsGalois extension F⊆E there exists a polynomial p∈F[X] that is separable and splits over E; E is a splitting field of p over F.
Русский
Для любой конечномерной Галуа-об extension F⊆E существует многочлен p∈F[X], который разделим над E и распадается в поле E; E является разворачивающим полем p над F.
LaTeX
$$$\exists p\in F[X]\; (p\;\text{Separable}) \land (p\;\text{IsSplittingField } F E)$$$
Lean4
theorem is_separable_splitting_field [FiniteDimensional F E] [IsGalois F E] :
∃ p : F[X], p.Separable ∧ p.IsSplittingField F E :=
by
obtain ⟨α, h1⟩ := Field.exists_primitive_element F E
use minpoly F α, separable F α, IsGalois.splits F α
rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← h1]
rw [IntermediateField.adjoin_simple_toSubalgebra_of_integral (integral F α)]
apply Algebra.adjoin_mono
rw [Set.singleton_subset_iff, Polynomial.mem_rootSet]
exact ⟨minpoly.ne_zero (integral F α), minpoly.aeval _ _⟩
