proposition: Lemma normedTI_Dade : Dade_hypothesis G L A.
proof: Proof. have [[sAG notA1] [_ _ /eqP defL]] := (subsetD1P sAG1, and3P tiAG). have [_ sLG tiAG_L] := normedTI_memJ_P tiAG. split=> // [|a b Aa Ab /imsetP[x Gx def_b]|]. - rewrite /(A <| L) -{2}defL subsetIr andbT; apply/subsetP=> a Aa. by rewrite -(tiAG_L a) ?(subsetP sAG) // conjgE mulKg. - by rewrite def_b imset_f // -(tiAG_L a) -?def_b. exists (fun _ => 1%G) => [a Aa | a b _ _]; last by rewrite cards1 coprime1n. by rewrite sdprod1g -(setIidPl sLG) -setIA (setIidPr (cent1_normedTI tiAG Aa)). 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)