for f being Polynomial of F_Complex
for z being Element of F_Complex st z <> 0. F_Complex holds
( f is Hurwitz iff z * f is Hurwitz )