proposition: Corollary coprime_odd_faithful_cent_abelem gT p (A G E : {group gT}) : E \in 'E_p(G) -> p.-group G -> A \subset 'N(G) -> coprime #|G| #|A| -> odd #|G| -> A \subset 'C('Ldiv_p('C_G(E))) -> A \subset 'C(G).
proof: Proof. case/pElemP=> sEG abelE pG nGA coGA oddG cCEA. have [-> | ntG] := eqsVneq G 1; first by rewrite cents1. have [p_pr _ _] := pgroup_pdiv pG ntG. have{} cCEA: A \subset 'C('Ohm_1('C_G(E))). by rewrite (OhmE 1 (pgroupS _ pG)) ?subsetIl ?cent_gen. apply: coprime_nil_faithful_cent_stab (pgroup_nil pG) _ => //. rewrite subsetI subsetIl centsC /=; set CC := 'C_G(_). have sCCG: CC \subset G := subsetIl _ _; have pCC := pgroupS sCCG pG. rewrite (coprime_odd_faithful_Ohm1 pCC) ?(coprimeSg sCCG) ?(oddSg sCCG) //. by rewrite !(normsI, norms_cent, normG). rewrite (subset_trans cCEA) // centS // OhmS // setIS // centS //. rewrite subsetI sEG /= centsC (subset_trans cCEA) // centS //. have cEE: abelian E := abelem_abelian abelE. by rewrite -{1}(Ohm1_id abelE) OhmS // subsetI sEG. 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)