:: deftheorem DefaddCoset defines addCoset ZMODUL04:def 2 :
for V being Z_Module st V is Mult-cancelable holds
for b₂ being BinOp of (Class (EQRZM V)) holds
( b₂ = addCoset V iff for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds
b₂ . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) );