proposition: Lemma mulmx_sum_row m n (u : 'rV_m) (A : 'M_(m, n)) : u *m A = \sum_i u 0 i *: row i A.
proof: Proof. by apply/rowP => j /[!(mxE, summxE)]; apply: eq_bigr => i _ /[!mxE]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)