theorem ThSPDM2: :: ZMODLAT2:25

for L being positive-definite Z_Lattice
for v being Vector of (DivisibleMod L) holds
( (ScProductDM L) . (v,v) = 0 iff v = 0. (DivisibleMod L) )