proposition: Lemma cfdot_classfun_part p1 p2 : '[ '1_[p1], '1_[p2] ] = #|'SG_m|%:R^-1 * #|classCT p1|%:R * (p1 == p2)%:R.
proof: Proof. rewrite /cfdot /= -mulrA; congr (_ * _). case: (altP eqP) => [<-{p2} | /negbTE Hneq]; rewrite /= ?mulr1 ?mulr0. - rewrite (bigID (fun x => x \in classCT p1)) /=. under eq_bigr => i /andP[_]. rewrite -classCTP !cfuniCTE => -> /=. by rewrite mul1r conjC1 over. rewrite sumr_const /= big1 ?addr0; first last => [i /andP[_]|]. rewrite -classCTP !cfuniCTE => /negbTE -> /=. by rewrite mul0r. congr _%:R; apply eq_card => /= x. by rewrite unfold_in inE. - apply big1 => i _; rewrite !cfuniCTE. case: eqP => [-> | _]; rewrite /= ?mul0r // mul1r {i}. by rewrite partnCTE /= !CTpartnK Hneq /= conjC0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg fingroup morphism perm gproduct) mathcomp(ssrnum matrix vector mxalgebra algC) mathcomp(classfun character mxrepresentation) tools ordcast partition sorted permcomp cycles cycletype permcent