English
If ζ is a primitive root of n, then IsCyclotomicExtension {n} A C iff C = adjoin A { ζ }.
Русский
Если ζ — примитивный корень n-й степени, то IsCyclotomicExtension {n} A C эквивално C = adjoin A { ζ }.
LaTeX
$$$\\text{IsCyclotomicExtension}\\left(\\{n\\}\\right)\\;A\\;C \\iff C = \\operatorname{adjoin}_A\\{\\zeta\\}$$$
Lean4
theorem isCyclotomicExtension_singleton_iff_eq_adjoin (C : Subalgebra A B) {ζ : B} (hζ : IsPrimitiveRoot ζ n) :
IsCyclotomicExtension { n } A C ↔ C = adjoin A { ζ } :=
by
rw [isCyclotomicExtension_iff_eq_adjoin]
· simp only [Set.mem_singleton_iff, exists_eq_left]
suffices adjoin A {b | n ≠ 0 ∧ b ^ n = 1} = adjoin A { ζ } by rw [this]
apply le_antisymm
· refine adjoin_le fun x ⟨_, hx⟩ ↦ ?_
obtain ⟨k, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton A ζ) _
· exact adjoin_mono <| Set.singleton_subset_iff.mpr ⟨NeZero.ne n, hζ.pow_eq_one⟩
· simpa only [Set.mem_singleton_iff, ne_eq, forall_eq, NeZero.ne n, not_false_eq_true, forall_const] using ⟨ζ, hζ⟩
