:: deftheorem defB2DB defines B2DB ZMODLAT3:def 9 :
for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for b₃ being Function of I,(DualBasis I) holds
( b₃ = B2DB I iff ( dom b₃ = I & rng b₃ = DualBasis I & ( for v being Vector of (EMLat L) st v in I holds
( (ScProductDM L) . (v,(b₃ . v)) = 1 & ( for w being Vector of (EMLat L) st w in I & v <> w holds
(ScProductDM L) . (w,(b₃ . v)) = 0 ) ) ) ) );