:: deftheorem defines is_primitive_root_of_degree POLYNOM8:def 6 :
for L being non empty well-unital doubleLoopStr
for x being Element of L
for n being Element of NAT holds
( x is_primitive_root_of_degree n iff ( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds
x |^ i <> 1. L ) ) );