Lemma pointwise_prod_stdb_vector {n : nat} (v : Vector R n) (i : ⟦ n ⟧%stn) : v *pw (stdb_vector i) = scalar_lmult_vec (v i) (stdb_vector i). Proof. apply funextfun. intros j. unfold scalar_lmult_vec, vector_fmap, pointwise. destruct (stn_eq_or_neq i j) as [i_eq_j | i_neq_j]. - rewrite i_eq_j; apply idpath. - unfold stdb_vector. rewrite (stn_eq_or_neq_right i_neq_j). now do 2 rewrite rigmultx0. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.GaussianElimination.Auxiliary.