:: deftheorem Def9 defines lmultCoset ZMODUL02:def 9 :
for V being Z_Module
for W being Submodule of V
for b₃ being Function of [: the carrier of INT.Ring,(CosetSet (V,W)):],(CosetSet (V,W)) holds
( b₃ = lmultCoset (V,W) iff for z being Element of INT.Ring
for A being Element of CosetSet (V,W)
for a being VECTOR of V st A = a + W holds
b₃ . (z,A) = (z * a) + W );