Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 5 / d

Write the determinant in its Leibniz formula for determinants, where $S_n$ is the set of permutations of $\{1,\dots ,n\}$:The permutation sign is justified by the given row-interchange property: a permutation matrix is obtained from the identity matrix by row interchanges, and every interchange changes its determinant by a factor $-1$. Reversing a sequence of interchanges constructs the inverse permutation with the same number of interchanges. Consequently $\mathrm{sgn}({\sigma }^{-1})=\mathrm{sgn}(\sigma )$. The Leibniz formula for determinants can itself be obtained by expanding the rows multilinearly in the standard basis: repeated selected coordinate rows contribute zero, and the remaining terms are precisely these signed permutation matrices.

Since $(A^T{)}_{ij}=a_{ji}$, the same formula givesReindex the product with $j=\sigma (i)$ and reindex the sum with $\tau ={\sigma }^{-1}$. Both reindexings are bijections, soThus $\det (A)=\det (A^T)$ for every real square matrix, including singular matrices. This proof does not assume the analogous column-operation rules in order to establish the transpose identity.