English
If there exists a primitive root for every n ∈ S with n ≠ 0 in M, there is a K-algebra isomorphism as above.
Русский
Если существует примитивный корень для каждого n ∈ S, n ≠ 0 в M, существует вышеупомянутый K-алгебраический изоморфизм.
LaTeX
$$$\\exists \\varphi: L \\cong_K \\operatorname{adjoin}_K\\{ x \\in M \\mid \\exists n \\in S, n \\neq 0 \\land x^n = 1 \\}$$$
Lean4
/-- If `IsCyclotomicExtension {n} K L`, then `L` is the splitting field of `X ^ n - 1`. -/
theorem isSplittingField_X_pow_sub_one : IsSplittingField K L (X ^ n - 1) :=
{ splits' := splits_X_pow_sub_one K L (mem_singleton n)
adjoin_rootSet' := by
rw [← ((iff_adjoin_eq_top { n } K L).1 inferInstance).2]
congr
refine Set.ext fun x => ?_
simp only [mem_singleton_iff, ne_eq, exists_eq_left, NeZero.ne, not_false_eq_true, true_and, mem_setOf_eq]
simp only [mem_rootSet', map_sub, map_pow, aeval_one, aeval_X, sub_eq_zero, map_X, and_iff_right_iff_imp,
Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one]
exact fun _ => X_pow_sub_C_ne_zero (NeZero.pos n) (1 : L) }
