proposition: Lemma cfAut_Dade_coherent calS tau1 chi : coherent_with calS L^# tau tau1 -> (1 < #|[set i | 'chi_i \in calS]|)%N /\ cfAut_closed u calS -> chi \in irr L -> chi \in calS -> (tau1 chi)^u = tau1 (chi^u).
proof: Proof. case=> [[Itau1 Ztau1] tau1_tau] [irrS_gt1 sSuS] /irrP[i {chi}->] Schi. have sSZS: {subset calS <= 'Z[calS]} by move=> phi Sphi; apply: mem_zchar. pose mu j := 'chi_j 1%g *: 'chi_i - 'chi_i 1%g *: 'chi_j. have ZAmu j: 'chi_j \in calS -> mu j \in 'Z[calS, L^#]. move=> Sxj; rewrite zcharD1E !cfunE mulrC subrr. by rewrite rpredB //= scale_zchar ?sSZS // ?Cint_Cnat ?Cnat_irr1. have Npsi j: 'chi_j \in calS -> '[tau1 'chi_j] = 1%:R. by move=> Sxj; rewrite Itau1 ?sSZS ?cfnorm_irr. have{Npsi} Dtau1 Sxj := vchar_norm1P (Ztau1 _ (sSZS _ Sxj)) (Npsi _ Sxj). have [e [r tau1_chi]] := Dtau1 _ Schi; set eps := (-1) ^+ e in tau1_chi. have{} Dtau1 j: 'chi_j \in calS -> exists t, tau1 'chi_j = eps *: 'chi_t. move=> Sxj; suffices: 0 <= (eps *: tau1 'chi_j) 1%g. have [f [t ->]] := Dtau1 j Sxj. have [-> | neq_f_eps] := eqVneq f e; first by exists t. rewrite scalerA -signr_addb scaler_sign addbC -negb_eqb neq_f_eps. by rewrite cfunE oppr_ge0 lt_geF ?irr1_gt0. rewrite -(pmulr_rge0 _ (irr1_gt0 i)) cfunE mulrCA. have: tau1 (mu j) 1%g == 0 by rewrite tau1_tau ?ZAmu ?Dade1. rewrite raddfB 2?raddfZ_Cnat ?Cnat_irr1 // !cfunE subr_eq0 => /eqP <-. by rewrite tau1_chi cfunE mulrCA signrMK mulr_ge0 ?Cnat_ge0 ?Cnat_irr1. have SuSirr j: 'chi_j \in calS -> 'chi_(aut_Iirr u j) \in calS. by rewrite aut_IirrE => /sSuS. have [j Sxj neq_ij]: exists2 j, 'chi_j \in calS & 'chi_i != 'chi_j. move: irrS_gt1; rewrite (cardsD1 i) inE Schi ltnS card_gt0 => /set0Pn[j]. by rewrite !inE -(inj_eq irr_inj) eq_sym => /andP[]; exists j. have: (tau1 (mu j))^u == tau1 (mu j)^u. by rewrite !tau1_tau ?cfAut_zchar ?ZAmu ?Dade_aut. rewrite !raddfB [-%R]lock !raddfZ_Cnat ?Cnat_irr1 //= -lock -!aut_IirrE. have [/Dtau1[ru ->] /Dtau1[tu ->]] := (SuSirr i Schi, SuSirr j Sxj). have: (tau1 'chi_i)^u != (tau1 'chi_j)^u. apply: contraNneq neq_ij => /cfAut_inj/(isometry_raddf_inj Itau1)/eqP. by apply; rewrite ?sSZS //; apply: rpredB. have /Dtau1[t ->] := Sxj; rewrite tau1_chi !cfAutZ_Cint ?rpred_sign //. rewrite !scalerA -!(mulrC eps) -!scalerA -!scalerBr -!aut_IirrE. rewrite !(inj_eq (scalerI _)) ?signr_eq0 // (inj_eq irr_inj) => /negPf neq_urt. have [/CnatP[a ->] /CnatP[b xj1]] := (Cnat_irr1 i, Cnat_irr1 j). rewrite xj1 eq_subZnat_irr neq_urt orbF andbC => /andP[_]. by rewrite eqn0Ngt -ltC_nat -xj1 irr1_gt0 /= => /eqP->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)