English
IsCyclotomicExtension is equivalent to the conjunction of: (a) every n in S has a primitive root, and (b) the subalgebra generated by the roots of unity of orders in S is the whole ambient algebra.
Русский
IsCyclotomicExtension эквивалентно сочетанию: (а) для каждого n в S существует примитивный корень, и (б) подалгебра, порожденная корнями единицы степеней из S, есть всякая база.
LaTeX
$$$ IsCyclotomicExtension S A B \\iff (\\forall n \\in S, IsPrimitiveRoot \\ a n) \\land adjoin A \\{ b \\mid \\exists n \\in S, b^n = 1\\} = \\top $$$
Lean4
/-- A reformulation of `IsCyclotomicExtension` that uses `⊤`. -/
theorem iff_adjoin_eq_top :
IsCyclotomicExtension S A B ↔
(∀ n : ℕ, n ∈ S → n ≠ 0 → ∃ r : B, IsPrimitiveRoot r n) ∧
adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1} = ⊤ :=
⟨fun h => ⟨fun _ => h.exists_isPrimitiveRoot, Algebra.eq_top_iff.2 h.adjoin_roots⟩, fun h =>
⟨h.1 _, Algebra.eq_top_iff.1 h.2⟩⟩
