:: deftheorem defEmbedding defines EMbedding ZMODUL08:def 3 :
for V being torsion-free Z_Module
for b₂ being strict Z_Module holds
( b₂ = EMbedding V iff ( the carrier of b₂ = rng (MorphsZQ V) & the ZeroF of b₂ = zeroCoset V & the addF of b₂ = (addCoset V) || (rng (MorphsZQ V)) & the lmult of b₂ = (lmultCoset V) | [:INT,(rng (MorphsZQ V)):] ) );