proposition: Lemma Dade_normedTI_P : reflect (A != set0 /\ {in A, forall a, H a = 1%G}) (normedTI A G L).
proof: Proof. apply: (iffP idP) => [tiAG | [nzA trivH]]. split=> [|a Aa]; first by have [] := andP tiAG. apply/trivGP; rewrite -(coprime_TIg (coHL Aa Aa)) subsetIidl subsetI cHA. by rewrite (subset_trans (normal_sub (nsHC a))) ?(cent1_normedTI tiAG). apply/normedTI_memJ_P; split=> // a g Aa Gg. apply/idP/idP=> [Aag | Lg]; last by rewrite memJ_norm ?(subsetP nAL). have /imsetP[k Lk def_ag] := conjAG Aa Aag (imset_f _ Gg). suffices: (g * k^-1)%g \in 'C_G[a]. by rewrite -Dade_sdprod ?trivH // sdprod1g inE groupMr ?groupV // => /andP[]. rewrite !inE groupM ?groupV // ?(subsetP sLG) //=. by rewrite conjg_set1 conjgM def_ag conjgK. 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)