theorem :: ZMODLAT1:16

for L being positive-definite Z_Lattice
for v being Vector of L holds
( ||.v.|| = 0 iff v = 0. L ) by ThSc6, defPositive;