The Exercise

Corollary 2.4 of Nielsen and Chuang is the singular value decomposition. The matrix $A$ is any square matrix with real or complex entries, for instance the matrix of an operator on the state space of a quantum system in an orthonormal basis; nothing more is asked of it. The corollary writes $A$ as a product of three factors: a unitary matrix, a diagonal matrix whose entries are nonnegative real numbers, and a second unitary matrix.^✦ The diagonal entries are the singular values of $A$.

The Claim

A unitary matrix $U$ is a square matrix whose conjugate transpose $U^\dagger$ is its inverse, $$U^\dagger U = U U^\dagger = I .$$(1) Over the real numbers $U^\dagger$ is the transpose, and a unitary matrix is an orthogonal one.

For real numbers $d_1, \dots, d_n$, the diagonal matrix $\operatorname{diag}(d_1, \dots, d_n)$ is the $n \times n$ matrix with $d_i$ in its $i$th diagonal entry and zeros elsewhere.

What Is Checked

The claim is stated over $n \times n$ matrices with real or complex entries, for every size $n$, and over the unitary matrices (1) and the diagonal matrices of the same size and field. What the library proves about them is the decomposition (2) of every such matrix.