English
If for all n ∈ S there exists a primitive root, then IsCyclotomicExtension S K (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b^n = 1}).
Русский
Если для всех n ∈ S существует примитивный корень, то IsCyclotomicExtension S K (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b^n = 1}).
LaTeX
$$$\\forall n\\in S, \\exists r: L, IsPrimitiveRoot(r,n) \\Rightarrow IsCyclotomicExtension S K (IntermediateField.adjoin K \\{b : L | ∃ n ∈ S, n \\neq 0 ∧ b^n = 1\\})$$$
Lean4
/-- A cyclotomic extension splits `X ^ n - 1` if `n ∈ S`. -/
theorem splits_X_pow_sub_one [H : IsCyclotomicExtension S K L] (hS : n ∈ S) : Splits (algebraMap K L) (X ^ n - 1) :=
by
rw [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X]
obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS (NeZero.ne _)
exact X_pow_sub_one_splits hz
