let L be positive-definite RATional Z_Lattice; :: thesis: for b being OrdBasis of DualLat L holds GramMatrix ((InnerProduct (DualLat L)),b) is Matrix of dim L,F_Rat
let b be OrdBasis of DualLat L; :: thesis: GramMatrix ((InnerProduct (DualLat L)),b) is Matrix of dim L,F_Rat
A1: the scalar of (DualLat L) = (ScProductDM L) || the carrier of (DualLat L) by defDualLat;
A2: DualLat L is Submodule of DivisibleMod L by ThDL2;
dim L = dim (DualLat L) by ThRankDL;
hence GramMatrix ((InnerProduct (DualLat L)),b) is Matrix of dim L,F_Rat by A1, A2, ThSLGM2; :: thesis: verum