:: deftheorem defDualBasis defines DualBasis ZMODLAT3:def 8 :
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for b₃ being Subset of (DivisibleMod L) holds
( b₃ = DualBasis I iff for v being Vector of (DivisibleMod L) holds
( v in b₃ iff ex u being Vector of (EMLat L) st
( u in I & (ScProductDM L) . (u,v) = 1 & ( for w being Vector of (EMLat L) st w in I & u <> w holds
(ScProductDM L) . (w,v) = 0 ) ) ) );