English
In the setting of a finite extension L/K with all nth roots of unity in K, the following three conditions are equivalent: (i) Galois and cyclic automorphism group; (ii) existence of an irreducible X^n − C a with L splitting; (iii) L = K(α) for some α with α^n in K.
Русский
В условии конечного расширения L/K, где K содержит все корни единицы n-го порядка, три условия эквивалентны: (i) Галуа и циклическая группа автоморфизмов; (ii) существует Irreducible X^n − C a, для которого L является разворачивающим; (iii) существует α в L такие, что L = K(α) и α^n ∈ K.
LaTeX
$$$\text{IsGalois}(K,L) \wedge \text{IsCyclic}(L \simeq_K L) \;\leftrightarrow\; \exists a\in K:\ Irreducible(X^n - C a) \wedge IsSplittingField(K,L,X^n - C a) \;\leftrightarrow\; \exists α\in L:\ α^n \in \mathrm{range}(\mathrm{algebraMap}_{K,L}) \wedge K⟮α⟯ = ⊤.$$$
Lean4
theorem isCyclic_of_isSplittingField_X_pow_sub_C [NeZero n] : IsCyclic (L ≃ₐ[K] L) :=
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
isCyclic_of_surjective _ (autEquivZmod H _ <| (mem_primitiveRoots hn).mp hζ.choose_spec).symm.surjective
