proposition: Lemma Clifford_astab : H <*> 'C_G(H) \subset 'C([set: sH] | 'Cl).
proof: Proof. rewrite join_subG !subsetI sHG subsetIl /=; apply/andP; split. apply/subsetP=> h Hh /[1!inE]; have Gh := subsetP sHG h Hh. apply/subsetP=> W _; have simW := socle_simple W; have [modW _ _] := simW. have simWh: mxsimple rH (socle_base W *m rG h) by apply: Clifford_simple. rewrite inE -val_eqE /= PackSocleK eq_sym. apply/component_mx_isoP; rewrite ?subgK //; apply: component_mx_iso => //. by apply: submx_trans (component_mx_id simW); move/mxmoduleP: modW => ->. apply/subsetP=> z cHz /[1!inE]; have [Gz _] := setIP cHz. apply/subsetP=> W _; have simW := socle_simple W; have [modW _ _] := simW. have simWz: mxsimple rH (socle_base W *m rG z) by apply: Clifford_simple. rewrite inE -val_eqE /= PackSocleK eq_sym. by apply/component_mx_isoP; rewrite ?subgK //; apply: Clifford_iso. 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)