proposition: Lemma col_vec_mult_eq { m n : nat } (mat : Matrix R m n) (v1 : Vector R n) (v2 : Vector R m) (e : (mat ** (col_vec v1)) = col_vec v2) : ∏ i : (stn m), Σ ((mat i) *pw v1) = v2 i.
proof: Proof. now apply toforallpaths; use col_vec_inj. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.Algebra.RigsAndRings UniMath.Algebra.IteratedBinaryOperations UniMath.Algebra.Matrix UniMath.Algebra.Domains_and_Fields UniMath.Algebra.GaussianElimination.Auxiliary UniMath.Algebra.GaussianElimination.Vectors