Determinant of a Real Square Matrix

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$, with $[n]$ as in Intervals of Natural Numbers (ii), and let $A\in\mathcal{M}_{n}(\mathbb{R})$ be a square real matrix with entries $A_{ij}$, with the set $S_{n}$ of permutations of $[n]$, the sign $\operatorname{sgn}:S_{n}\to\mathbb{R}$, and sums and products as in Commutative Rings, Fields and Ordered Fields: Standard Notation (iii).

(i) The determinant $\det:\mathcal{M}_{n}(\mathbb{R})\to\mathbb{R}$ is the map $D_{n}$ of The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique (ii), so that

$$\det A=\sum_{\sigma\in S_{n}}\operatorname{sgn}(\sigma)\prod_{i\in[n]}A_{i\sigma(i)}.$$