The Determinant of a Positive Definite Matrix Is Positive

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\in\mathbb{N}$ and let $\Sigma\in\mathcal{S}(n)$ be a symmetric real $n\times n$ matrix that is positive definite, with the matrix product, the transpose, the determinant $\det$, invertible matrices and square roots of nonnegative real numbers.

(i) Positivity. $\det\Sigma>0$.

(ii) Factors. If a real $n\times n$ matrix $A\in\mathcal{M}_{n}(\mathbb{R})$ satisfies $AA^{\top}=\Sigma$, then $A$ is invertible and

$$|\det A|=\sqrt{\det\Sigma}$$

($\det\Sigma>0$ by (i)).