proposition: Lemma coprime_cent_quotient_pgroup : 'C(T / M) = 'C(T) / M.
proof: Proof. symmetry; rewrite -quotientInorm -quotientMidl -['C(T / M)]cosetpreK. congr (_ / M); set Cq := _ @*^-1 _; set C := 'N_('C(T))(M). suffices <-: 'N_Cq(T) = C. rewrite setIC group_modl ?sub_cosetpre //= -/Cq; apply/setIidPr. rewrite -quotientSK ?subsetIl // cosetpreK. by rewrite -coprime_norm_quotient_pgroup cent_sub. apply/eqP; rewrite eqEsubset subsetI -sub_quotient_pre ?subsetIr //. rewrite quotientInorm quotient_cents //= andbC subIset ?cent_sub //=. have nMC': 'N_Cq(T) \subset 'N(M) by rewrite subIset ?subsetIl. rewrite subsetI nMC' andbT (sameP commG1P trivgP) /=. rewrite -(coprime_TIg coMT) subsetI commg_subr subsetIr andbT. by rewrite -quotient_cents2 ?sub_quotient_pre ?subsetIl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)