proposition: Lemma component_mx_def : {I : finType & {W : I -> 'M_n | forall i, mx_iso U (W i) & compU = \sum_i W i}}%MS.
proof: Proof. pose r i := row i iso_u; pose r_nz i := r i != 0; pose I := {i | r_nz i}. exists I; exists (fun i => cyclic_mx (r (sval i))) => [i|]. apply/mxsimple_isoP=> //; apply/and3P. split; first by rewrite cyclic_mx_module. apply/rowV0Pn; exists (r (sval i)); last exact: (svalP i). by rewrite sub_capmx cyclic_mx_id row_sub. have [f hom_u_f <-] := @row_hom_mxP u (r (sval i)) (row_sub _ _). by rewrite defU -hom_cyclic_mx ?mxrankM_maxl. rewrite -(eq_bigr _ (fun _ _ => genmx_id _)) -genmx_sums -genmx_component. rewrite [in compU]unlock; apply/genmxP/andP; split; last first. by apply/sumsmx_subP => i _; rewrite (sumsmx_sup (sval i)). apply/sumsmx_subP => i _. case i0: (r_nz i); first by rewrite (sumsmx_sup (Sub i i0)). by move/negbFE: i0; rewrite -cyclic_mx_eq0 => /eqP->; apply: sub0mx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)