theorem LmEMDetX3: :: ZMODLAT3:41

for L being positive-definite Z_Lattice
for b being OrdBasis of L
for e being OrdBasis of EMLat L st e = (MorphsZQ L) * b holds
GramMatrix ((InnerProduct L),b) = GramMatrix ((InnerProduct (EMLat L)),e)