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-resit/5/c/solution

First add row 1 to rows 2 and 3. This is the product of two elementary matrices, written compactly as
Swap rows 2 and 4 with , then subtract half of the new row 2 from row 3 with :
This gives the upper triangular matrix
Because , rearranging yields the convention , where
The conjugation by moves the earlier elimination multipliers to the appropriate rows. Ignoring this permutation when forming would give an incorrect PLU factorization. Here the same permutation is its own inverse, so also holds.

New to topics? Read the docs here!