let L be RATional Z_Lattice; :: thesis: for b being OrdBasis of L holds Det (GramMatrix b) in F_Rat

let b be OrdBasis of L; :: thesis: Det (GramMatrix b) in F_Rat

GramMatrix b is Matrix of dim L,F_Rat by ThGM1;

hence Det (GramMatrix b) in F_Rat by LmGM11; :: thesis: verum

let b be OrdBasis of L; :: thesis: Det (GramMatrix b) in F_Rat

GramMatrix b is Matrix of dim L,F_Rat by ThGM1;

hence Det (GramMatrix b) in F_Rat by LmGM11; :: thesis: verum