theorem :: MATRIX_7:17

for K being Field
for n being Nat
for A being Matrix of n,K st n >= 1 & A is diagonal holds
Det A = the multF of K $$ (diagonal_of_Matrix A)