proposition: Lemma FTtype1_irr_partition : partition [set Si in [seq S_ chi | chi <- calS]] calX.
proof: Proof. apply/and3P; split; last 1 first. - rewrite inE; apply/mapP=> [[chi Schi /esym/setP S_0]]. have /eqP[] := seqInd_neq0 nsHL Schi. rewrite [chi]cfun_sum_constt big1 // => i chi_i. by have:= S_0 i; rewrite inE chi_i inE. - apply/eqP/setP=> i; apply/bigcupP/FTtype1_irrP=> [[S_chi] | [chi Schi Si]]. by rewrite inE => /mapP[chi Schi ->]; exists chi. by exists (S_ chi); rewrite // inE map_f. apply/trivIsetP=> S_chi1 S_chi2. rewrite !inE => /mapP[chi1 Schi1 ->] /mapP[chi2 Schi2 ->] {S_chi1 S_chi2}chi2'1. apply/pred0P=> i; rewrite /= !inE; apply/andP=> [[chi1_i chi2_i]]. suffices: '['chi_i] == 0 by rewrite cfnorm_irr oner_eq0. rewrite (constt_ortho_char (seqInd_char Schi1) (seqInd_char Schi2)) //. by rewrite (seqInd_ortho _ Schi1 Schi2) // (contraNneq _ chi2'1) // => ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)