:: deftheorem defDivisibleVector defines divisible ZMODUL08:def 1 :
for V being Z_Module
for v being Vector of V holds
( v is divisible iff for a being Element of INT.Ring st a <> 0. INT.Ring holds
ex u being Vector of V st a * u = v );