:: deftheorem defEMLat defines EMLat ZMODLAT2:def 4 :
for L being Z_Lattice
for b₂ being strict Z_Lattice holds
( b₂ = EMLat L iff ( the carrier of b₂ = rng (MorphsZQ L) & the ZeroF of b₂ = zeroCoset L & the addF of b₂ = (addCoset L) || (rng (MorphsZQ L)) & the lmult of b₂ = (lmultCoset L) | [: the carrier of INT.Ring,(rng (MorphsZQ L)):] & the scalar of b₂ = ScProductEM L ) );