proposition: Lemma mulmx_diag n (d e : 'rV_n) : diag_mx d *m diag_mx e = diag_mx (\row_j (d 0 j * e 0 j)).
proof: Proof. by apply/matrixP=> i j; rewrite mul_diag_mx !mxE mulrnAr. 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)