let L be positive-definite Z_Lattice; :: thesis: GramDet (InnerProduct L) = GramDet (InnerProduct (EMLat L))
set b = the OrdBasis of L;
reconsider e = (MorphsZQ L) * the OrdBasis of L as OrdBasis of EMLat L by ZMODLAT2:41;
P1: GramMatrix ((InnerProduct L), the OrdBasis of L) = GramMatrix ((InnerProduct (EMLat L)),e) by LmEMDetX3;
GramDet (InnerProduct L) = Det (GramMatrix ((InnerProduct L), the OrdBasis of L)) by ZMODLAT1:def 35
.= Det (GramMatrix ((InnerProduct (EMLat L)),e)) by P1, ZMODLAT2:42
.= GramDet (InnerProduct (EMLat L)) by ZMODLAT1:def 35 ;
hence GramDet (InnerProduct L) = GramDet (InnerProduct (EMLat L)) ; :: thesis: verum