theorem :: ZMODLAT2:24

for L being INTegral Z_Lattice
for r being non zero Element of F_Rat
for a being Rational
for v, u being Vector of (EMLat (r,L)) st r = a holds
((a ") * (a ")) * <;v,u;> in INT