theorem LmDE311: :: ZMODLAT3:24

for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L ex a being Element of F_Real st
( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )