Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2014/digital-systems-linear-algebra-introduction-to-formal-proof/4/a/solution

Apply the elementary row operations from bottom to top: , , and . This order ensures that each subtraction uses the original preceding row. The result is the upper triangular matrix
Put , , , . Row is either zero if , or has its first nonzero entry in column . Thus, for arbitrary real parameters, a row echelon form is obtained by retaining the nonzero rows of in their existing order and moving every zero row to the bottom. This deals explicitly with vanishing parameters; an upper triangular matrix with an intermediate zero row is not yet a row echelon form.
The subtractions preserve the determinant, so the original matrix has
A square matrix is invertible exactly when its determinant is nonzero. Consequently,
These conditions concern consecutive parameters: no ordering, positivity, or pairwise distinctness of all four is required. More generally the rank of a matrix here is the number of nonzero , because the retained nonzero rows have distinct leading columns.

New to topics? Read the docs here!