proposition: Lemma rfix_mx_conjsg (H : {set gT}) x : x \in G -> H \subset G -> (rfix_mx (H :^ x) :=: rfix_mx H *m rG x)%MS.
proof: Proof. move=> Gx sHG; pose rf y := rfix_mx (H :^ y). suffices{x Gx} IH: {in G &, forall y z, rf y *m rG z <= rf (y * z)%g}%MS. apply/eqmxP; rewrite -/(rf x) -[H]conjsg1 -/(rf 1%g). rewrite -{4}[x] mul1g -{1}[rf x](repr_mxKV rG Gx) -{1}(mulgV x). by rewrite submxMr IH ?groupV. move=> x y Gx Gy; apply/rfix_mxP=> zxy; rewrite actM => /imsetP[zx Hzx ->]. have Gzx: zx \in G by apply: subsetP Hzx; rewrite conj_subG. rewrite -mulmxA -repr_mxM ?groupM ?groupV // -conjgC repr_mxM // mulmxA. by rewrite rfix_mx_id. 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)