:: deftheorem defines is_primitive_root_of INT_8:def 3 :
for i, n being Nat holds
( i is_primitive_root_of n iff order (i,n) = Euler n );