:: deftheorem defines alternating BILINEAR:def 27 :
for K being Fanoian Field
for V being non empty ModuleStr over K
for f being additiveFAF additiveSAF Form of V,V holds
( f is alternating iff for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) );