theorem LmDE21: :: ZMODLAT3:30

for L being Z_Lattice
for v being Vector of (DivisibleMod L)
for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring ) holds
v is Dual of L