proposition: Lemma diag_mx_seq_deltar m n (i : 'I_m) (j : 'I_n) (s : seq R) : diag_mx_seq m m s *m delta_mx i j = s`_i *: delta_mx i j.
proof: Proof. apply/matrixP=> k l; rewrite !mxE (bigD1 k) //= big1 ?addr0. rewrite !mxE eqxx; case: (eqVneq k i)=>[->/=|_]; last by rewrite !mulr0. by case: eqP. move=> p; rewrite !mxE=> /negbTE; rewrite (inj_eq (@ord_inj _)) eq_sym=> ->. by rewrite mul0r. 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