English
Let K be a field, n > 0, and a ∈ K such that X^n − a is irreducible over K. If L/K is a splitting field of X^n − a and α ∈ L satisfies α^n = a, then the smallest subfield of L containing K and α equals L; i.e., K(α) = L.
Русский
Пусть K — поле, n > 0 и a ∈ K так, что X^n − a ирредуцируем над K. Пусть L/K — разворачивающее поле X^n − a, и α ∈ L удовлетворяет α^n = a. Тогда минимальное подполе L, содержащее K и α, совпадает с L; то есть K(α) = L.
LaTeX
$$$\text{Let } K \text{ be a field } n \in \mathbb{N}, \ n>0, \text{ and } a \in K \text{ with } X^n - a \ \text{ irreducible over } K. \text{ If } L/K \text{ is the splitting field of } X^n - C a \text{ and } \alpha \in L \text{ satisfies }\alpha^n = \mathrm{algebraMap}_{K,L}(a), \text{ then } K\langle \alpha \rangle = L.$$$
Lean4
theorem adjoin_root_eq_top_of_isSplittingField : K⟮α⟯ = ⊤ :=
by
refine (IntermediateField.eq_adjoin_of_eq_algebra_adjoin _ _ _ ?_).symm
exact (Algebra.adjoin_root_eq_top_of_isSplittingField hζ H hα).symm
