:: deftheorem Def11 defines Mult_Mod_pV ZMODUL02:def 11 :
for p being prime Element of INT.Ring
for V being Z_Module
for b₃ being Function of [: the carrier of (GF p), the carrier of (VectQuot (V,(p (*) V))):], the carrier of (VectQuot (V,(p (*) V))) holds
( b₃ = Mult_Mod_pV (V,p) iff for a being Element of (GF p)
for i being Element of INT.Ring
for x being Element of (VectQuot (V,(p (*) V))) st a = i mod p holds
b₃ . (a,x) = (i mod p) * x );