∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : CommRing R] [IsDomain R] [Finite F] {n : ℕ} [NeZero n]
  {χ : MulChar F R} {μ : R},
  χ ^ n = 1 → IsPrimitiveRoot μ n → ∀ {x : F}, x ≠ 0 → ∃ z ∈ Algebra.adjoin ℤ {μ}, χ x - 1 = z * (μ - 1)