:: deftheorem defines Z_MQ_VectSp ZMODUL02:def 12 :
for p being prime Element of INT.Ring
for V being Z_Module holds Z_MQ_VectSp (V,p) = ModuleStr(# the carrier of (VectQuot (V,(p (*) V))), the addF of (VectQuot (V,(p (*) V))), the ZeroF of (VectQuot (V,(p (*) V))),(Mult_Mod_pV (V,p)) #);