proposition: Proposition coprime_nil_faithful_cent_stab gT (A G : {group gT}) : A \subset 'N(G) -> coprime #|G| #|A| -> nilpotent G -> let C := 'C_G(A) in 'C_G(C) \subset C -> A \subset 'C(G).
proof: Proof. move=> nGA coGA nilG C; rewrite subsetI subsetIl centsC /= -/C => cCA. pose N := 'N_G(C); have sNG: N \subset G by rewrite subsetIl. have sCG: C \subset G by rewrite subsetIl. suffices cNA : A \subset 'C(N). rewrite centsC (sameP setIidPl eqP) -(nilpotent_sub_norm nilG sCG) //= -/C. by rewrite subsetI subsetIl centsC. have{nilG} solN: solvable N by rewrite (solvableS sNG) ?nilpotent_sol. rewrite (stable_factor_cent cCA) ?(coprimeSg sNG) /stable_factor //= -/N -/C. rewrite subcent_normal subsetI (subset_trans (commSg A sNG)) ?commg_subl //=. rewrite comm_norm_cent_cent 1?centsC ?subsetIr // normsI // !norms_norm //. by rewrite cents_norm 1?centsC ?subsetIr. 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)