English
IsCyclotomicExtension for a singleton {n} is equivalent to existence of a primitive root for n and the adjoint generated by n-th roots of unity equals the whole B when n is fixed.
Русский
IsCyclotomicExtension для синглтёна {n} эквивалентно существованию примитивного корня для n и тому, что порожденная степенью n корней единицы образует всю B.
LaTeX
$$IsCyclotomicExtension {n} A B ↔ (∃ r ∈ B, IsPrimitiveRoot r n) ∧ ∀ x ∈ adjoin A {b ∈ B | b^n = 1}, x$$
Lean4
@[nontriviality]
theorem subsingleton_iff [Subsingleton B] : IsCyclotomicExtension S A B ↔ S ⊆ {0, 1} :=
by
have : Subsingleton (Subalgebra A B) := inferInstance
refine ⟨fun ⟨hprim, _⟩ ↦ ?_, fun hS ↦ ?_⟩
· refine subset_pair_iff.mpr fun s hs ↦ or_iff_not_imp_left.mpr fun hs' ↦ ?_
obtain ⟨ζ, hζ⟩ := hprim hs hs'
exact mod_cast hζ.unique (IsPrimitiveRoot.of_subsingleton ζ)
· refine ⟨fun {s} hs hs' ↦ ?_, fun x ↦ by convert (mem_top (R := A) : x ∈ ⊤)⟩
· have : s = 1 := (subset_pair_iff.mp hS s hs).resolve_left hs'
exact ⟨0, this ▸ IsPrimitiveRoot.of_subsingleton 0⟩
