:: deftheorem defines signnorm HERMITAN:def 9 :
for V being non empty ModuleStr over F_Complex
for f being Form of V,V
for v being Vector of V holds signnorm (f,v) = Re (f . (v,v));