proposition: Lemma mx_Schur_iso U V f : mxsimple U -> mxsimple V -> (U <= dom_hom_mx f)%MS -> (U *m f <= V)%MS -> U *m f != 0 -> mx_iso U V.
proof: Proof. move=> simU simV homUf sUfV nzUf; have [modU _ _] := simU. have [g invg homUg defUg] := mx_Schur_inj_iso simU homUf nzUf. exists g => //; apply: mx_Schur_onto; rewrite ?defUg //. by rewrite -!submx0 defUg in nzUf *. 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)