:: deftheorem defines GramMatrix ZMODLAT1:def 37 :
for L being Z_Lattice
for b being OrdBasis of L holds GramMatrix b = GramMatrix ((InnerProduct L),b);