proposition: Lemma mx_iso_simple U V : mx_iso U V -> mxsimple U -> mxsimple V.
proof: Proof. move=> isoUV [modU nzU simU]; have [f injf homUf defV] := isoUV. split=> [||W modW sWV nzW]; first by rewrite (mx_iso_module isoUV). by rewrite -(eqmx_eq0 defV) -(mul0mx n f) (can_eq (mulmxK injf)). rewrite -defV -[W](mulmxKV injf) submxMr //; set W' := W *m _. have sW'U: (W' <= U)%MS by rewrite -[U](mulmxK injf) submxMr ?defV. rewrite (simU W') //; last by rewrite -(can_eq (mulmxK injf)) mul0mx mulmxKV. rewrite hom_mxmodule ?dom_hom_invmx // -[W](mulmxKV injf) submxMr //. exact: submx_trans sW'U homUf. 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)