English
If L/K is {n}-cyclotomic, then L is the splitting field of X^n - 1 over K.
Русский
Если L/K циклотомическое по {n}, то L — разворачивающее поле для многочлена X^n - 1 над K.
LaTeX
$$$IsCyclotomicExtension\\{n\\} K L \\Rightarrow IsSplittingField(K,L,X^n-1)$$$
Lean4
/-- If `IsCyclotomicExtension {n} K L`, then `L` is the splitting field of `cyclotomic n K`. -/
theorem splitting_field_cyclotomic : IsSplittingField K L (cyclotomic n K) :=
{ splits' := splits_cyclotomic K L (mem_singleton n)
adjoin_rootSet' := by
rw [← ((iff_adjoin_eq_top { n } K L).1 inferInstance).2]
letI := Classical.decEq L
obtain ⟨ζ : L, hζ⟩ := IsCyclotomicExtension.exists_isPrimitiveRoot K L (mem_singleton n) (NeZero.ne _)
exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ }