proposition: Lemma Dade_Ind_restr_J : {in L & calP, forall x B, 'Ind[G] 'aa_(B :^ x) = 'Ind[G] 'aa_B}.
proof: Proof. move=> x B Lx dB; have [defMB [sBA _]] := (Dade_set_sdprod dB, setIdP dB). have dBx: B :^ x \in calP. by rewrite !inE -{2}(normsP nAL x Lx) conjSg -!cards_eq0 cardJg in dB *. have defHBx: 'H(B :^ x) = 'H(B) :^ x. rewrite /'H(_) (big_imset _ (in2W (conjg_inj x))) -bigcapJ /=. by apply: eq_bigr => a Ba; rewrite DadeJ ?(subsetP sBA). have defNBx: 'N_L(B :^ x) = 'N_L(B) :^ x by rewrite conjIg -normJ (conjGid Lx). have [_ mulHNB _ tiHNB] := sdprodP defMB. have defMBx: 'M(B :^ x) = 'M(B) :^ x. rewrite -mulHNB conjsMg -defHBx -defNBx. by case/sdprodP: (Dade_set_sdprod dBx). have def_aa_x y: 'aa_(B :^ x) (y ^ x) = 'aa_B y. rewrite !rDadeE // defMBx memJ_conjg !mulrb -mulHNB defHBx defNBx. have [[h z Hh Nz ->] | // ] := mulsgP. by rewrite conjMg !remgrMid ?cfunJ ?memJ_conjg // -conjIg tiHNB conjs1g. apply/cfunP=> y; have Gx := subsetP sLG x Lx. rewrite [eq]lock !cfIndE ?sMG //= {1}defMBx cardJg -lock; congr (_ * _). rewrite (reindex_astabs 'R x) ?astabsR //=. by apply: eq_bigr => z _; rewrite conjgM def_aa_x. 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)