:: deftheorem defPositive defines positive-definite ZMODLAT1:def 6 :
for IT being Z_Lattice holds
( IT is positive-definite iff for v being Vector of IT st v <> 0. IT holds
||.v.|| > 0 );