## Singular values of a matrix

### Set

 context $A \in \mathrm{SquareMatrix}(n,\mathbb C)$
 definiendum $\sqrt{\lambda} \in \mathrm{SingularVal}(A)$
 postulate $\lambda \in \mathrm{EigenVal}(A^*A)$

### Discussion

Note that $A^*A$ is always Hermitian positive semi-definite matrix.

Singular values make sense for more general operators too.