for L being RATional Z_Lattice
for LX being Z_Lattice
for b being OrdBasis of LX st LX is Submodule of DivisibleMod L & the scalar of LX = (ScProductDM L) || the carrier of LX holds
GramMatrix ((InnerProduct LX),b) is Matrix of dim LX,F_Rat