:: deftheorem defrEMLat defines EMLat ZMODLAT2:def 5 :
for L being Z_Lattice
for r being Element of F_Rat
for b₃ being strict Z_Lattice holds
( b₃ = EMLat (r,L) iff ( the carrier of b₃ = r * (rng (MorphsZQ L)) & the ZeroF of b₃ = zeroCoset L & the addF of b₃ = (addCoset L) || (r * (rng (MorphsZQ L))) & the lmult of b₃ = (lmultCoset L) | [: the carrier of INT.Ring,(r * (rng (MorphsZQ L))):] & the scalar of b₃ = (ScProductDM L) || (r * (rng (MorphsZQ L))) ) );