proposition: Lemma inertia_bigdprod phi (Phi := cfBigdprod defG phi) : Phi 1%g != 0 -> 'I_L[Phi] = L :&: \bigcap_(i | P i) 'I_L[phi i].
proof: Proof. move=> nz_Phi; apply/eqP; rewrite eqEsubset; apply/andP; split. rewrite subsetI Inertia_sub; apply/bigcapsP=> i Pi. have [] := cfBigdprodK nz_Phi Pi; move: (_ / _) => a nz_a <-. by rewrite inertia_scale_nz ?sub_inertia_Res //= ?nAL. rewrite subsetI subsetIl; apply: subset_trans (inertia_prod _ _ _). apply: setISS. by rewrite -(bigdprodWY defG) norms_gen ?norms_bigcup //; apply/bigcapsP. apply/bigcapsP=> i Pi; rewrite (bigcap_min i) //. by rewrite -inertia_bigdprodi ?subsetIr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop prime order) mathcomp(ssralg ssrnum finset fingroup morphism perm) mathcomp(automorphism quotient action zmodp cyclic center) mathcomp(gproduct commutator gseries nilpotent pgroup) mathcomp(sylow maximal frobenius matrix mxalgebra) mathcomp(mxrepresentation vector algC classfun character) mathcomp(archimedean)