Sage will create random matrices and vectors, sometimes with various properties. These can be very useful for quick experiments, and they are also useful for illustrating that theorems hold for any object satisfying the hypotheses of the theorem. But this will never replace a proof.
We will illustrate Theorem NME1 using Sage. We will use a variant of the random_matrix() constructor that uses the algorithm='unimodular' keyword. We will have to wait for Chapter D before we can give a full explanation, but for now, understand that this command will always create a square matrix that is nonsingular. Also realize that there are square nonsingular matrices which will never be the output of this command. In other words, this command creates elements of just a subset of all possible nonsingular matrices.
So we are using random matrices below to illustrate properties predicted by Theorem NME1. Execute the first command to create a random nonsingular matrix, and notice that we only have to mark the output of A as random for our automated testing process. After a few runs, notice that you can also edit the value of n to create matrices of different sizes. With a matrix A defined, run the next three cells, which by Theorem NME1 each always produce True as their output, no matter what value A has, so long as A is nonsingular. Read the code and try to determine exactly how they correspond to the parts of the theorem (some commentary along these lines follows).
The only portion of these commands that may be unfamilar is the last one. The command range(n) is incredibly useful, as it will create a list of the integers from 0 up to, but not including, n. (We saw this command briefly in Sage FDV.) So, for example, range(3) == [0,1,2] is True. Pivots are returned as a “tuple” which is very much like a list, except we cannot change the contents. We can see the difference by the way the tuple prints with parentheses ((,)) rather than brackets ([,]). We can convert a list to a tuple with the tuple() command, in order to make the comparison succeed.
How do we tell if the reduced row-echelon form of the augmented matrix of a system of equations represents a system with a unique solution? First, the system must be consistent, which by Theorem RCLS means the last column is not a pivot column. Then with a consistent system we need to insure there are no free variables. This happens if and only if the remaining columns are all pivot columns, according to Theorem FVCS, thus the test used in the last compute cell.