:: deftheorem defriV defines EMbedding ZMODUL08:def 6 :
for V being torsion-free Z_Module
for r being Element of F_Rat
for b₃ being strict Z_Module holds
( b₃ = EMbedding (r,V) iff ( the carrier of b₃ = r * (rng (MorphsZQ V)) & the ZeroF of b₃ = zeroCoset V & the addF of b₃ = (addCoset V) || (r * (rng (MorphsZQ V))) & the lmult of b₃ = (lmultCoset V) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ V))):] ) );