:: deftheorem defines InnerProduct ZMODLAT1:def 36 :
for L being Z_Lattice holds InnerProduct L = the scalar of L;