proposition: Lemma mulmx_sum_col : forall {R : comRingType} m n (u : 'cV[R]_n) (A : 'M_(m, n)), A *m u = \sum_i u i 0 *: col i A.
proof: Proof. move=> R m n u A; apply/colP=> j; rewrite mxE summxE; apply: eq_bigr => i _. by rewrite !mxE mulrC. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2