:: deftheorem defDivisibleMod defines DivisibleMod ZMODUL08:def 4 :
for V being torsion-free Z_Module
for b₂ being strict Z_Module holds
( b₂ = DivisibleMod V iff ( the carrier of b₂ = Class (EQRZM V) & the ZeroF of b₂ = zeroCoset V & the addF of b₂ = addCoset V & the lmult of b₂ = (lmultCoset V) | [:INT,(Class (EQRZM V)):] ) );