proposition: Lemma eq_in_cycTIiso (i : Iirr W) (phi : 'CF(G)) : phi \in dirr G -> {in V, phi =1 'chi_i} -> phi = sigma 'chi_i.
proof: Proof. move=> Dphi; rewrite -(inv_dprod_IirrK defW i). case: (inv_dprod_Iirr _)=> /= i1 j1 EphiC. pose psi : 'CF(G) := eta_ i1 j1 - phi. have ZpsiV: {in V, forall g, psi g = 0}=> [g GiV|]. by rewrite /psi !cfunE cycTIiso_restrict // -(EphiC _ GiV) subrr. pose a i j := '[psi, eta_ i j]; pose S := [set ij | a ij.1 ij.2 != 0]. case: (boolP ((i1, j1) \in S))=> [I1J1iS|]; last first. rewrite inE negbK /a cfdotBl cfdot_cycTIiso !eqxx /=. rewrite cfdot_dirr ?(irr_dirr, cycTIiso_dirr) //. case: (boolP (phi == _))=> [|_]. by rewrite opprK -(natrD _ 1 1) pnatr_eq0. case: (boolP (phi == _))=> [/eqP //|]. by rewrite subr0 oner_eq0. have SPos : (0 < #|S|)%N by rewrite (cardD1 (i1,j1)) I1J1iS. have SLt: (#|S| <= 2)%N. by rewrite -[2%N]add1n cycTI_NC_sub // !cycTI_NC_dirr // cycTIiso_dirr. have: (0 < #|S| < 2 * minn w1 w2)%N. rewrite SPos; apply: leq_ltn_trans SLt _. by rewrite -{1}[2%N]muln1 ltn_mul2l /= leq_min ![(1 < _)%N]ltnW. move/(cycTI_NC_minn ZpsiV); rewrite leqNgt; case/negP. by apply: leq_ltn_trans SLt _; rewrite leq_min w1gt2. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)