ThmDex – An index of mathematical definitions, results, and conjectures.
Determinant of real diagonal matrix
Formulation 0
Let $A \in \mathbb{R}^{N \times N}$ be a D6160: Real square matrix such that
(i) \begin{equation} A = \begin{bmatrix} A_{1, 1} & 0 & \cdots & 0 \\ 0 & A_{2, 2} & \vdots & 0 \\ \vdots & \cdots & \ddots & \vdots \\ 0 & 0 & \cdots & A_{N, N} \end{bmatrix} \end{equation}
Then \begin{equation} \text{Det} A = \prod_{n = 1}^N A_{n, n} \end{equation}
Subresults
R2463: Determinant of a real identity matrix
R4107: Determinant of real diagonal matrix with constant diagonal
Proofs
Proof 0
Let $A \in \mathbb{R}^{N \times N}$ be a D6160: Real square matrix such that
(i) \begin{equation} A = \begin{bmatrix} A_{1, 1} & 0 & \cdots & 0 \\ 0 & A_{2, 2} & \vdots & 0 \\ \vdots & \cdots & \ddots & \vdots \\ 0 & 0 & \cdots & A_{N, N} \end{bmatrix} \end{equation}
Since $A$ is a diagonal matrix, then the product $\prod_{n = 1}^N A_{n, \pi(n)}$ contains a zero factor and thus equals zero for every permutation $\pi \in S_N$ except for the identity permutation $1 2 3 \cdots N$, although it may equal zero in this case also if the diagonal has zeros. Thus, applying results
(i) R4097: Real arithmetic expression for real matrix determinant
(ii) R4098: Sign of identity permutation

we have \begin{equation} \begin{split} \text{det}(A) & = \sum_{\pi \in S_N} \left( \text{sign}(\pi) \prod_{n = 1}^N A_{n, \pi(n)} \right) \\ & = \text{sign}(1 2 3 \cdots N) \prod_{n = 1}^N A_{n, n} \\ & = \prod_{n = 1}^N A_{n, n} \end{split} \end{equation} $\square$