proposition: Lemma Dade_vchar alpha : alpha \in 'Z[irr L, A] -> alpha^\tau \in 'Z[irr G].
proof: Proof. rewrite [alpha \in _]zchar_split => /andP[Zaa CFaa]. rewrite Dade_expansion // rpredN rpred_sum // => B dB. suffices calP_B: B \in calP. by rewrite rpredZsign cfInd_vchar // Dade_restriction_vchar. case/imsetP: dB => B0 /setIdP[sB0A notB00] defB. have [x Lx ->]: exists2 x, x \in L & B = B0 :^ x. by apply/imsetP; rewrite defB (mem_repr B0) ?orbit_refl. by rewrite inE -cards_eq0 cardJg cards_eq0 -(normsP nAL x Lx) conjSg sB0A. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius ssrnum) mathcomp(matrix mxalgebra mxrepresentation vector algC classfun character) mathcomp(inertia vcharacter) odd_order(PFsection1)