theorem LmGM11: :: ZMODLAT2:55

for n being Nat
for M being Matrix of n,F_Real st M is Matrix of n,F_Rat holds
Det M in F_Rat