:: deftheorem defines -root POLYEQ_5:def 1 :
for n being non zero Nat
for z being Complex holds n -root z = (n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i>));