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. 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.
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.