∀ {K : Type u_1} [inst : Field K] {n : ℕ} {a : K} {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L},
  (primitiveRoots n K).Nonempty →
    Irreducible (Polynomial.X ^ n - Polynomial.C a) →
      ∀ (hα : α ^ n = (algebraMap K L) a),
        Function.Bijective ⇑(AdjoinRoot.liftAlgHom (Polynomial.X ^ n - Polynomial.C a) (Algebra.ofId K L) α ⋯)