:: deftheorem defDualElement defines Dual ZMODLAT3:def 5 :
for L being Z_Lattice
for b₂ being Vector of (DivisibleMod L) holds
( b₂ is Dual of L iff for v being Vector of (DivisibleMod L) st v in EMbedding L holds
(ScProductDM L) . (b₂,v) in INT.Ring );