proposition: Lemma mxsimple_isoP U V : mxsimple U -> reflect (mx_iso U V) (mxsimple_iso U V).
proof: Proof. move=> simU; pose u := nz_row U. have [Uu nz_u]: (u <= U)%MS /\ u != 0 by rewrite nz_row_sub nz_row_mxsimple. apply: (iffP and3P) => [[modV] | isoUV]; last first. split; last by rewrite (mxrank_iso isoUV). by case: (mx_iso_simple isoUV simU). have [f injf homUf defV] := isoUV; apply/rowV0Pn; exists (u *m f). rewrite sub_capmx -defV submxMr //. by apply/row_hom_mxP; exists f; first apply: (submx_trans Uu). by rewrite -(mul0mx _ f) (can_eq (mulmxK injf)) nz_u. case/rowV0Pn=> v; rewrite sub_capmx => /andP[Vv]. case/row_hom_mxP => f homMf def_v nz_v eqrUV. pose uG := cyclic_mx u; pose vG := cyclic_mx v. have def_vG: (uG *m f :=: vG)%MS by rewrite /vG -def_v; apply: hom_cyclic_mx. have defU: (U :=: uG)%MS by apply: mxsimple_cyclic. have mod_uG: mxmodule uG by rewrite cyclic_mx_module. have homUf: (U <= dom_hom_mx f)%MS. by rewrite defU cyclic_mx_sub ?dom_hom_mx_module. have isoUf: mx_iso U (U *m f). apply: mx_Schur_inj_iso => //; apply: contra nz_v; rewrite -!submx0. by rewrite (eqmxMr f defU) def_vG; apply: submx_trans (cyclic_mx_id v). apply: mx_iso_trans (isoUf) (eqmx_iso _); apply/eqmxP. have sUfV: (U *m f <= V)%MS by rewrite (eqmxMr f defU) def_vG cyclic_mx_sub. by rewrite -mxrank_leqif_eq ?eqn_leq 1?mxrankS // -(mxrank_iso isoUf). 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)