proposition: Lemma scalar_mult_matrix_product { n } ( r : ⟦ n ⟧%stn ) ( s1 s2 : F ) : ((scalar_mult_row_matrix r s1 ) **' (scalar_mult_row_matrix r s2 )) = (scalar_mult_row_matrix r (s1 * s2)%ring ).
proof: Proof. rewrite scalar_mult_as_matrix. unfold scalar_mult_row. unfold scalar_mult_row_matrix. apply funextfun; intros i. apply funextfun; intros j. destruct (stn_eq_or_neq i r); simpl coprod_rect. 2: { reflexivity. } unfold pointwise. apply pathsinv0, rigassoc2. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.Matrix UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors UniMath.Algebra.GaussianElimination.Matrices