:: deftheorem defines even ZMODLAT1:def 7 :
for IT being INTegral Z_Lattice holds
( IT is even iff for v being Vector of IT holds ||.v.|| is even );