proposition: Lemma diag_mx_sum_delta n (d : 'rV_n) : diag_mx d = \sum_i d 0 i *: delta_mx i i.
proof: Proof. apply/matrixP=> i j; rewrite summxE (bigD1_ord i) //= !mxE eqxx /=. by rewrite eq_sym mulr_natr big1 ?addr0 // => i'; rewrite !mxE eq_liftF mulr0. 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)