proposition: Lemma card_afix_irr_classes (ito : action A (Iirr G)) (cto : action A _) a : a \in A -> [acts A, on classes G | cto] -> (forall i x y, x \in G -> y \in cto (x ^: G) a -> 'chi_i x = 'chi_(ito i a) y) -> #|'Fix_ito[a]| = #|'Fix_(classes G | cto)[a]|.
proof: Proof. move=> Aa actsAG stabAchi; apply/eqP; rewrite -eqC_nat; apply/eqP. have [[cP cK] iCK] := (irr_classP, irr_classK, class_IirrK). pose icto b i := iC (cto (c i) b). have Gca i: cto (c i) a \in classes G by rewrite (acts_act actsAG). have inj_qa: injective (icto a). by apply: can_inj (icto a^-1%g) _ => i; rewrite /icto iCK ?actKin ?cK. pose Pa : 'M[algC]_(Nirr G) := perm_mx (actperm ito a). pose qa := perm inj_qa; pose Qa : 'M[algC]_(Nirr G) := perm_mx qa^-1^-1%g. transitivity (\tr Pa). rewrite -sumr_const big_mkcond; apply: eq_bigr => i _. by rewrite !mxE permE inE sub1set inE; case: ifP. symmetry; transitivity (\tr Qa). rewrite cardsE -sumr_const -big_filter_cond big_mkcond big_filter /=. rewrite reindex_irr_class; apply: eq_bigr => i _; rewrite !mxE invgK permE. by rewrite inE sub1set inE -(can_eq cK) iCK //; case: ifP. rewrite -[Pa](mulmxK uX) -[Qa](mulKmx uX) mxtrace_mulC; congr (\tr(_ *m _)). rewrite -row_permE -col_permE; apply/matrixP=> i j; rewrite !mxE. rewrite -{2}[j](permKV qa); move: {j}(_ j) => j; rewrite !permE iCK //. apply: stabAchi; first by case/repr_classesP: (cP j). by rewrite repr_irr_classK (mem_repr_classes (Gca _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)