English
For any ζ that is a primitive root of n, the singleton cyclotomic extension is generated by ζ; i.e., IsCyclotomicExtension {n} A (adjoin A {ζ}).
Русский
Для любого ζ, являющегося примитивным корнем степени n, циклотомическое расширение порождается ζ; то есть IsCyclotomicExtension {n} A (adjoin A {ζ}).
LaTeX
$$$\\text{IsCyclotomicExtension}\\left(\\{n\\}\\right)\\;A\\;\\operatorname{adjoin}_A\\{\\zeta\\}$$$
Lean4
theorem mem_of_pow_eq_one (C : Subalgebra A B) [h : IsCyclotomicExtension S A C] {m : ℕ} {ζ : B} (h₁ : m ∈ S)
(h₂ : m ≠ 0) (hζ : ζ ^ m = 1) : ζ ∈ C := by
obtain ⟨η, hη⟩ := h.1 h₁ h₂
replace hη := hη.map_of_injective (FaithfulSMul.algebraMap_injective C B)
have : NeZero m := ⟨h₂⟩
obtain ⟨k, _, rfl⟩ := hη.eq_pow_of_pow_eq_one hζ
rw [← map_pow]
exact Subalgebra.pow_mem _ η.prop _
