:: deftheorem defines rho LMOD_XX1:def 28 :
for R being comRing
for M being LeftMod of R holds rho M = id M;