proposition: Lemma mx_iso_component V : mx_iso U V -> (V <= compU)%MS.
proof: Proof. move=> isoUV; have [f injf homUf defV] := isoUV. have simV := mx_iso_simple isoUV simU. have hom_u_f := submx_trans Uu homUf. have ->: (V :=: cyclic_mx (u *m f))%MS. apply: eqmx_trans (hom_cyclic_mx hom_u_f). exact: eqmx_trans (eqmx_sym defV) (eqmxMr _ defU). have iso_uf: (u *m f <= iso_u)%MS by apply/row_hom_mxP; exists f. rewrite genmxE; apply/row_subP=> j; rewrite row_mul mul_rV_lin1 /=. set a := vec_mx _; apply: submx_trans (submxMr _ iso_uf) _. apply/row_subP=> i; rewrite row_mul [in compU]unlock (sumsmx_sup i) //. by apply/cyclic_mxP; exists a; rewrite // vec_mxK row_sub. 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)