Lemma scalar_mult_as_matrix {m n : nat} (r : ⟦ m ⟧%stn) (s : F) (mat : Matrix F m n) : ((scalar_mult_row_matrix r s) **' mat) = scalar_mult_row r s mat. Proof. use funextfun; intros i; use funextfun; intros ?. unfold matrix_mult, scalar_mult_row_matrix, scalar_mult_row, row. destruct (stn_eq_or_neq i r) as [? | ?]. - simpl coprod_rect. etrans. { apply maponpaths. etrans. { apply maponpaths_2, (@pointwise_comm2_vector F). } apply pointwise_assoc2_vector. } use sum_stdb_vector_pointwise_prod. - simpl coprod_rect. use sum_stdb_vector_pointwise_prod. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices.