proposition: Lemma Dade_irr_sub_conjC chi (phi := chi - chi^*%CF) : chi \in irr L -> chi \in 'CF(L, 1%g |: A) -> exists t, phi^\tau = 'chi_t - ('chi_t)^*%CF.
proof: Proof. case/irrP=> i Dchi Achi; rewrite {chi}Dchi in phi Achi *. have [Rchi | notRchi] := eqVneq (conjC_Iirr i) i. by exists 0; rewrite irr0 cfConjC_cfun1 /phi -conjC_IirrE Rchi !subrr linear0. have Zphi: phi \in 'Z[irr L, A]. have notA1: 1%g \notin A by have [] := ddA. by rewrite -(setU1K notA1) sub_conjC_vchar // zchar_split irr_vchar. have Zphi_tau: phi^\tau \in 'Z[irr G, G^#]. by rewrite zchar_split Dade_cfun Dade_vchar ?Zphi. have norm_phi_tau : '[phi^\tau] = 2%:R. rewrite Dade_isometry ?(zchar_on Zphi) // cfnormB -conjC_IirrE. by rewrite !cfdot_irr !eqxx eq_sym (negPf notRchi) add0r rmorph0 subr0. have [j [k ne_kj phi_tau]] := vchar_norm2 Zphi_tau norm_phi_tau. suffices def_k: conjC_Iirr j = k by exists j; rewrite -conjC_IirrE def_k. have/esym:= eq_subZnat_irr 1 1 k j (conjC_Iirr j) (conjC_Iirr k). rewrite (negPf ne_kj) orbF /= !scale1r !conjC_IirrE -rmorphB. rewrite -['chi_k - _]opprB -phi_tau /= -Dade_conjC // rmorphB /= cfConjCK. by rewrite -linearN opprB eqxx => /andP[/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)