proposition: Lemma Dade_set_sdprod : {in calP, forall B, 'H(B) ><| 'N_L(B) = 'M(B)}.
proof: Proof. move=> B /setIdP[sBA notB0]; apply: sdprodEY => /=. apply/subsetP=> x /setIP[Lx nBx]; rewrite inE. apply/bigcapsP=> a Ba; have Aa := subsetP sBA a Ba. by rewrite sub_conjg -DadeJ ?groupV // bigcap_inf // memJ_norm ?groupV. have /set0Pn[a Ba] := notB0; have Aa := subsetP sBA a Ba. have [_ /mulG_sub[sHaC _] _ tiHaL] := sdprodP (defCA Aa). rewrite -(setIidPl sLG) -setIA setICA (setIidPl sHaC) in tiHaL. by rewrite setICA ['H(B)](bigD1 a) //= !setIA tiHaL !setI1g. 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)