proposition: Lemma mxdiagZ a : \mxdiag_i (a%:M : 'M[R]_(p_ i)) = a%:M.
proof: Proof. apply/matrixP => s t; rewrite !mxE -(can_eq sigK) /sig1 /sig2. case: (sig s) (sig t) => [/= i j] [/= i' j']. case: eqP => [<-|ni] in j' *; last by rewrite !mxE; case: eqVneq => // -[]. by rewrite conform_mx_id eq_Tagged/= mxE. 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)