:: deftheorem defines Mult-cancelable ZMODUL01:def 7 :
for R being Ring
for IT being LeftMod of R holds
( IT is Mult-cancelable iff for a being Element of R
for v being Vector of IT holds
( not a * v = 0. IT or a = 0. R or v = 0. IT ) );