theorem :: MATRIX_7:37

for n being Nat
for K being commutative Ring
for A being Matrix of n,K st n >= 1 holds
Det A = Det (A @)