proposition: Lemma mx_Schur_inj_iso U f : mxsimple U -> (U <= dom_hom_mx f)%MS -> U *m f != 0 -> mx_iso U (U *m f).
proof: Proof. move=> simU homUf nzUf; have [modU _ _] := simU. have eqUfU: \rank (U *m f) = \rank U by apply/mxrank_injP; rewrite mx_Schur_inj. have{eqUfU} [g invg defUf] := complete_unitmx eqUfU. suffices homUg: (U <= dom_hom_mx g)%MS by exists g; rewrite ?defUf. apply/hom_mxP=> x Gx; have [ux defUx] := submxP (mxmoduleP modU x Gx). by rewrite -defUf -(hom_mxP homUf) // defUx -!(mulmxA ux) defUf. 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)