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

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