proposition: Lemma diag_mx_seq_deltal m n (i : 'I_m) (j : 'I_n) (s : seq R) : delta_mx i j *m diag_mx_seq n n s = s`_j *: delta_mx i j.
proof: Proof. apply/matrixP=> k l; rewrite !mxE (bigD1 l) //= big1 ?addr0. rewrite !mxE eqxx; case: (eqVneq l j)=>[->/=|_]; last by rewrite andbF mulr0 mul0r. by rewrite andbT; case: eqP=> _; [rewrite mulr1 mul1r | rewrite mulr0 mul0r]. move=> p; rewrite !mxE=> /negbTE; rewrite (inj_eq (@ord_inj _))=> ->. by rewrite mulr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring