proposition: Lemma row_hom_mxP u v : reflect (exists2 f, u <= dom_hom_mx f & u *m f = v)%MS (v <= row_hom_mx u)%MS.
proof: Proof. apply: (iffP sub_bigcapmxP) => [iso_uv | [f hom_uf <-] i _]. have{iso_uv} uv0 A: (A \in E_G)%MS /\ u *m A = 0 -> v *m A = 0. move/annihilator_mxP=> /submxP[a defA]. rewrite -[A]mxvecK {A}defA [a *m _]mulmx_sum_row !linear_sum big1 // => i _. by rewrite !linearZ /= (sub_kermxP _) ?scaler0 ?iso_uv. pose U := E_G *m lin_mul_row u; pose V := E_G *m lin_mul_row v. pose f := pinvmx U *m V. have hom_uv_f x: x \in G -> u *m rG x *m f = v *m rG x. move=> Gx; apply/eqP; rewrite 2!mulmxA mul_rV_lin1 -subr_eq0 -mulmxBr. rewrite uv0 // 2!linearB /= vec_mxK; split. by rewrite addmx_sub ?submxMl // eqmx_opp envelop_mx_id. have Uux: (u *m rG x <= U)%MS. by rewrite -(genmxE U) mxmodule_trans ?cyclic_mx_id ?cyclic_mx_module. by rewrite -{2}(mulmxKpV Uux) [_ *m U]mulmxA mul_rV_lin1 subrr. have def_uf: u *m f = v. by rewrite -[u]mulmx1 -[v]mulmx1 -(repr_mx1 rG) hom_uv_f. by exists f => //; apply/hom_mxP=> x Gx; rewrite def_uf hom_uv_f. apply/sub_kermxP; set A := vec_mx _. have: (A \in annihilator_mx u)%MS by rewrite vec_mxK row_sub. by case/annihilator_mxP => E_A uA0; rewrite -hom_envelop_mxC // uA0 mul0mx. 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)