:: deftheorem defines Hurwitz HURWITZ:def 8 :
for f being Polynomial of F_Complex holds
( f is Hurwitz iff for z being Element of F_Complex st z is_a_root_of f holds
Re z < 0 );