Gauss's method preserves the solution set

The declaration HefferonLinAlg.gauss_row_operations_preserve_solutions asserts the following. Let $K$ be an arbitrary field (commutative, with $0 \neq 1$; no further assumptions — no characteristic, ordering, algebraic-closure, or finiteness assumption), and let $m, n$ be arbitrary natural numbers, including $0$. Let $A = (A_{i,j})$ be an $m \times n$ matrix over $K$ (rows indexed by $\{0,\dots,m-1\}$, columns by $\{0,\dots,n-1\}$), let $b = (b_i) \in K^m$ be a column vector, let $M = (M_{i,k})$ be a square $m \times m$ matrix over $K$, and let $x = (x_j) \in K^n$ be a column vector; all five of $A$, $b$, $M$, $x$, together with $K$, $m$, $n$, are universally quantified, so the claim is made for every such choice. The single hypothesis is that $\det M$ is a unit of $K$ — since $K$ is a field this is exactly $\det M \neq 0$, i.e. $M$ is invertible; this hypothesis is satisfiable for every $m$ (e.g. $M = I_m$, and for $m = 0$ the empty determinant is $1$), so the statement is not vacuous. Under these assumptions the conclusion is the two-directional equivalence (if and only if) of the two vector equations

where all products are the usual ones over $K$: $(Ax)_i = \sum_{j} A_{i,j} x_j$ for $i < m$, $(MA)$ is the $m \times n$ matrix with entries $\sum_{k} M_{i,k} A_{k,j}$, $\bigl((MA)x\bigr)_i = \sum_{j} \bigl(\sum_k M_{i,k}A_{k,j}\bigr) x_j$, and $(Mb)_i = \sum_{k} M_{i,k} b_k$; equality of vectors means componentwise equality in every coordinate $i < m$. Note that the equivalence is asserted about one fixed vector $x$ at a time rather than being phrased as an equality of solution sets (though, $x$ being universally quantified, the claim ranges over all $x \in K^n$), that the statement says nothing about $M$ being an elementary matrix, a product of elementary matrices, or arising from any specific row operation — only that its determinant is invertible — and that it says nothing about the existence of any solution. Degenerate cases are silently included: when $m = 0$ there are no coordinates and both sides of the equivalence hold trivially for all data; when $n = 0$ the vector $x$ is empty, $Ax$ is the zero vector of $K^m$, and the assertion reduces to "$b = 0$ if and only if $Mb = 0$". Finally, the declaration is stated with its proof omitted (left as sorry), so nothing here is established by the file itself.