:: deftheorem defines ZMtoMQV ZMODUL02:def 13 :
for p being prime Element of INT.Ring
for V being Z_Module
for v being VECTOR of V holds ZMtoMQV (V,p,v) = v + (p (*) V);