proposition: Lemma Clifford_atrans : [transitive G, on [set: sH] | 'Cl].
proof: Proof. have [_ nz1 _] := irrG. apply: mxsimple_exists (mxmodule1 rH) nz1 _ _ => [[M simM _]]. pose W1 := PackSocle (component_socle sH simM). have [X sXG [def1 _]] := Clifford_basis simM; move/subsetP: sXG => sXG. apply/imsetP; exists W1; first by rewrite inE. symmetry; apply/setP=> W /[1!inE]; have simW := socle_simple W. have:= submx1 (socle_base W); rewrite -def1 -[(\sum_(x in X) _)%MS]mulmx1. case/(hom_mxsemisimple_iso simW) => [x Xx _ | | x Xx isoMxW]. - by apply: Clifford_simple; rewrite ?sXG. - exact: scalar_mx_hom. have Gx := sXG x Xx; apply/imsetP; exists x => //; apply/socleP/eqmxP/eqmx_sym. apply: eqmx_trans (val_Clifford_act _ Gx) _; rewrite PackSocleK. apply: eqmx_trans (eqmx_sym (Clifford_componentJ simM Gx)) _. apply/eqmxP; rewrite (sameP genmxP eqP) !{1}genmx_component. by apply/component_mx_isoP=> //; apply: Clifford_simple. 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)