:: deftheorem defines diagker BILINEAR:def 17 :
for K being ZeroStr
for V being non empty ModuleStr over K
for f being Form of V,V holds diagker f = { v where v is Vector of V : f . (v,v) = 0. K } ;