:: deftheorem defZero defines zeroCoset ZMODUL04:def 3 :
for V being Z_Module st V is Mult-cancelable holds
for b₂ being Element of Class (EQRZM V) holds
( b₂ = zeroCoset V iff for i being Integer st i <> 0 holds
b₂ = Class ((EQRZM V),[(0. V),i]) );