∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
  {ζ : B} {n : ℕ} [NeZero n],
  IsPrimitiveRoot ζ n →
    Algebra.adjoin A ((Polynomial.cyclotomic n A).rootSet B) = Algebra.adjoin A {b | ∃ a ∈ {n}, a ≠ 0 ∧ b ^ a = 1}