:: deftheorem defDualLat defines DualLat ZMODLAT3:def 10 :
for L being positive-definite RATional Z_Lattice
for b₂ being strict Z_Lattice holds
( b₂ = DualLat L iff ( the carrier of b₂ = DualSet L & 0. b₂ = 0. (DivisibleMod L) & the addF of b₂ = the addF of (DivisibleMod L) || the carrier of b₂ & the lmult of b₂ = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring, the carrier of b₂:] & the scalar of b₂ = (ScProductDM L) || the carrier of b₂ ) );