:: deftheorem DeflmultCoset defines lmultCoset ZMODUL04:def 4 :
for V being Z_Module st V is Mult-cancelable holds
for b₂ being Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) holds
( b₂ = lmultCoset V iff for q, A being object st q in RAT & A in Class (EQRZM V) holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds
b₂ . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)]) );