proposition: Lemma bigdprod_rowg m (I : finType) (P : pred I) A (B : 'M[F]_(m, n)) : let S := (\sum_(i | P i) A i)%MS in (S :=: B)%MS -> mxdirect S -> \big[dprod/1%g]_(i | P i) rowg (A i) = rowg B.
proof: Proof. move=> S defS; rewrite mxdirectE defS /= => /eqP rankB. apply: bigcprod_card_dprod (bigcprod_rowg defS) (eq_leq _). by rewrite card_rowg rankB expn_sum; apply: eq_bigr => i; rewrite card_rowg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient gproduct action finalg) mathcomp(zmodp commutator cyclic center pgroup gseries) mathcomp(nilpotent sylow maximal abelian matrix) mathcomp(mxalgebra mxrepresentation)