∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ} [inst_2 : ExpChar R p] [inst_3 : PerfectRing R p]
  {y : R}, (Polynomial.X ^ p - Polynomial.C y).roots = p • {(frobeniusEquiv R p).symm y}