:: deftheorem defines scalar-mult-cancelable CC0SP1:def 5 :
for V being non empty CLSStruct holds
( V is scalar-mult-cancelable iff for a being Complex
for v being Element of V holds
( not a * v = 0. V or a = 0 or v = 0. V ) );