proposition: Lemma abelem_rowgJ m (A : 'M_(m, n)) x : x \in G -> rV_E @* rowg (A *m rG x) = (rV_E @* rowg A) :^ x.
proof: Proof. move=> Gx; apply: (canRL (conjsgKV _)); apply/setP=> y. rewrite mem_conjgV !morphim_invmE !inE memJ_norm ?(subsetP nEG) //=. apply: andb_id2l => Ey; rewrite abelem_rV_J //. by rewrite submxMfree // row_free_unit (repr_mx_unit rG). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient gproduct action finalg) mathcomp(zmodp commutator cyclic center pgroup gseries) mathcomp(nilpotent sylow maximal abelian matrix) mathcomp(mxalgebra mxrepresentation)