:: deftheorem defines GramDet ZMODLAT1:def 38 :
for L being Z_Lattice holds GramDet L = GramDet (InnerProduct L);