proposition: Lemma mx_rsim_iso n (rG : reprG n) (U V : 'M_n) (modU : mxmodule rG U) (modV : mxmodule rG V) : mx_rsim (submod_repr modU) (submod_repr modV) <-> mx_iso rG U V.
proof: Proof. split=> [[B eqrUV injB homB] | [f injf homf defV]]. have: \rank (U *m val_submod (in_submod U 1%:M *m B)) = \rank U. do 2!rewrite mulmxA mxrankMfree ?row_base_free //. by rewrite -(eqmxMr _ (val_submod1 U)) -in_submodE val_submodK mxrank1. case/complete_unitmx => f injf defUf; exists f => //. apply/hom_mxP=> x Gx; rewrite -defUf -2!mulmxA -(val_submodJ modV) //. rewrite -(mulmxA _ B) -homB // val_submodE 3!(mulmxA U) (mulmxA _ _ B). rewrite -in_submodE -in_submodJ //. have [u ->] := submxP (mxmoduleP modU x Gx). by rewrite in_submodE -mulmxA -defUf !mulmxA !mulmx1. apply/eqmxP; rewrite -mxrank_leqif_eq. by rewrite mxrankMfree ?eqrUV ?row_free_unit. by rewrite -defUf mulmxA val_submodP. have eqrUV: \rank U = \rank V by rewrite -defV mxrankMfree ?row_free_unit. exists (in_submod V (val_submod 1%:M *m f)) => // [|x Gx]. rewrite /row_free {6}eqrUV -[_ == _]sub1mx -val_submodS. rewrite in_submodK; last by rewrite -defV submxMr ?val_submodP. by rewrite val_submod1 -defV submxMr ?val_submod1. rewrite -in_submodJ; last by rewrite -defV submxMr ?val_submodP. rewrite -(hom_mxP (submx_trans (val_submodP _) homf)) //. by rewrite -(val_submodJ modU) // mul1mx 2!(mulmxA ((submod_repr _) x)) -val_submodE. 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)