:: deftheorem defDualMod defines DualLatMod ZMODLAT3:def 7 :
for L being Z_Lattice
for b₂ being non empty strict LatticeStr over INT.Ring holds
( b₂ = DualLatMod L iff ( the carrier of b₂ = DualSet L & the addF of b₂ = the addF of (DivisibleMod L) || (DualSet L) & the ZeroF of b₂ = 0. (DivisibleMod L) & the lmult of b₂ = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,(DualSet L):] & the scalar of b₂ = (ScProductDM L) | [:(DualSet L),(DualSet L):] ) );