proposition: Lemma stable_rowg_mxK (L : {group rVn}) : [acts setT, on L | 'Zm] -> rowg (rowg_mx L) = L.
proof: Proof. move=> linL; apply/eqP; rewrite eqEsubset sub_rowg_mx andbT. apply/subsetP=> v; rewrite inE genmxE => /submxP[u ->{v}]. rewrite mulmx_sum_row group_prod // => i _. rewrite rowK; move: (enum_val i) (enum_valP i) => v Lv. have [->|] := eqVneq (u 0 i) 0; first by rewrite scale0r group1. by rewrite -unitfE => aP; rewrite ((actsP linL) (FinRing.Unit aP)) ?inE. 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)