proposition: Lemma diag_mx_seq_scale m n s (d : R) : d *: diag_mx_seq m n s = diag_mx_seq m n [seq d * x | x <- s].
proof: Proof. apply/matrixP=> i j; rewrite !mxE. case: eqP => _ /=; last by rewrite !mulr0n mulr0. have [hi|hl] := (ltnP i (size s)); first by rewrite (@nth_map _ 0). by rewrite ?nth_default ?mulr0 // size_map. 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