proposition: Lemma add_row_mult_as_matrix { m n } (r1 r2 : ⟦ m ⟧%stn) (ne : r1 ≠ r2) (s : R) (mat : Matrix R m n) : (add_row_mult_matrix r1 r2 s) **' mat = add_row_mult r1 r2 s mat.
proof: Proof. intros. apply funextfun; intros i; apply funextfun; intros j. unfold matrix_mult, add_row_mult_matrix, add_row_mult, col, row. destruct (stn_eq_or_neq i r2) as [i_eq_r2 | i_neq_r2]; simpl coprod_rect. - etrans. { apply maponpaths, (@pointwise_rdistr_vector R). } etrans. { apply vecsum_add. } apply map_on_two_paths. + etrans. 2: { apply maponpaths_2, i_eq_r2. } use sum_stdb_vector_pointwise_prod. + etrans. { apply vecsum_scalar_lmult. } apply maponpaths, @sum_stdb_vector_pointwise_prod. - use sum_stdb_vector_pointwise_prod. 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