theorem :: FIELD_16:38

for p being Prime
for R being commutative b₁ -characteristic Ring
for n being non zero Nat holds { (m * (1. R)) where m is Nat : m < p } c= Roots (X^ ((p |^ n),R))