theorem :: ZMATRLIN:47

for n being Nat
for M being Matrix of n,F_Real st M is Matrix of n,INT.Ring holds
Det M in INT by LmSign1A;