theorem :: ZMODUL03:37

for p being prime Element of INT.Ring
for V being free finite-rank Z_Module holds rank V = dim (Z_MQ_VectSp (V,p))