Gaussian elimination is not optimal, revisited

Although the end results are equations involving matrix products, our exposition builds upon previous works on the category of matrices (and the related category of finite vector spaces) which we extend by showing: why the direct sum (⊕,0) monoid is not closed, a biproduct encoding of Gaussian elimination, and how to further apply it in the derivation of linear algebra algorithms.