theorem Th52: :: MATRIXJ1:52

for m, n being Nat
for K being Field
for N being Matrix of n,K
for N1 being Matrix of m,K holds Det (block_diagonal (<*N,N1*>,(0. K))) = (Det N) * (Det N1)