proposition: Theorem Fchar_isometry f g : '[Fchar f | Fchar g] = '[f, g].
proof: Proof. Proof using Hn. rewrite (ncfuniCT_gen f) (ncfuniCT_gen g) !linear_sum /=. rewrite homsymdot_suml cfdot_suml; apply eq_bigr => la _. rewrite homsymdot_sumr cfdot_sumr; apply eq_bigr => mu _. rewrite ![Fchar (_ *: '1z_[_])]linearZ /= !Fchar_ncfuniCT. rewrite homsymdotZl homsymdotZr cfdotZl cfdotZr; congr (_ * (_ * _)). rewrite homsymdotpp // cfdotZl cfdotZr cfdot_classfun_part. case: (la =P mu) => [<-{mu} | _]; rewrite ?mulr0 ?mulr1 //. rewrite -zcoeffE -[LHS]mulr1; congr (_ * _). rewrite /zcoeff rmorphM rmorphV; first last. by rewrite unitfE pnatr_eq0 card_classCT_neq0. rewrite !rmorph_nat -mulrA [X in _ * X]mulrC - mulrA divff; first last. by rewrite pnatr_eq0 card_classCT_neq0. by rewrite mulr1 divff // pnatr_eq0 -lt0n cardsT card_Sn fact_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism gproduct) mathcomp(rat ssralg ssrint ssrnum algC vector archimedean) mathcomp(mxrepresentation classfun character) mathcomp(mpoly) sorted ordtype tools partition antisym sympoly homogsym Cauchy Schur_altdef stdtab therule permcomp cycletype towerSn permcent reprSn unitriginv MurnaghanNakayama