proposition: Lemma Clifford_simple M x : mxsimple rH M -> x \in G -> mxsimple rH (M *m rG x).
proof: Proof. have modmG m U y: y \in G -> (mxmodule rH) m U -> mxmodule rH (U *m rG y). move=> Gy modU; apply/mxmoduleP=> h Hh; have Gh := subsetP sHG h Hh. rewrite -mulmxA -repr_mxM // conjgCV repr_mxM ?groupJ ?groupV // mulmxA. by rewrite submxMr ?(mxmoduleP modU) // -mem_conjg (normsP nHG). have nzmG m y (U : 'M_(m, n)): y \in G -> (U *m rG y == 0) = (U == 0). by move=> Gy; rewrite -{1}(mul0mx m (rG y)) (can_eq (repr_mxK rG Gy)). case=> [modM nzM simM] Gx; have Gx' := groupVr Gx. split=> [||U modU sUMx nzU]; rewrite ?modmG ?nzmG //. rewrite -(repr_mxKV rG Gx U) submxMr //. by rewrite (simM (U *m _)) ?modmG ?nzmG // -(repr_mxK rG Gx M) submxMr. 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)