:: deftheorem defines positivediagvalued HERMITAN:def 13 :
for V being non empty ModuleStr over F_Complex
for f being Form of V,V holds
( f is positivediagvalued iff for v being Vector of V st v <> 0. V holds
0 < Re (f . (v,v)) );