Solution

ID: 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/solution

Write the determinant in its Leibniz formula for determinants, where is the set of permutations of :
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 . Reversing a sequence of interchanges constructs the inverse permutation with the same number of interchanges. Consequently . 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 , the same formula gives
Reindex the product with and reindex the sum with . Both reindexings are bijections, so
Thus 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.

New to topics? Read the docs here!