theorem :: FIELD_10:45
Roots (F_Complex,X^2+X+1) = {zeta,(zeta ^2)} by rootz;