∀ {F : Type u_1} [inst : Field F] [Finite F] {R : Type u_2} [inst_2 : CommRing R] [IsDomain R] {χ : MulChar F R} {n : ℕ}
  [NeZero n], χ ^ n = 1 → ∀ {μ : R}, IsPrimitiveRoot μ n → ∀ (a : F), χ a ∈ ℤ[μ]