:: deftheorem defGramDet defines GramDet ZMODLAT1:def 35 :
for V being free finite-rank Z_Module
for f being bilinear-FrForm of V,V
for b₃ being Element of F_Real holds
( b₃ = GramDet f iff for b being OrdBasis of V holds b₃ = Det (GramMatrix (f,b)) );