∀ {K : Type u} [inst : Field K] {n : ℕ} (a : K) (η : ↥(rootsOfUnity n K)),
  ((autAdjoinRootXPowSubC n a) η) (AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)) =
    ↑↑η • AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)