proposition: Lemma logn_quotient_cent_abelem gT p (A E : {group gT}) : A \subset 'N(E) -> p.-abelem E -> logn p #|E| <= 2 -> logn p #|A : 'C_A(E)| <= 1.
proof: Proof. move=> nEA abelE maxdimE; have [-> | ntE] := eqsVneq E 1. by rewrite (setIidPl (cents1 _)) indexgg logn1. pose rP := abelem_repr abelE ntE nEA. have [p_pr _ _] := pgroup_pdiv (abelem_pgroup abelE) ntE. have ->: 'C_A(E) = 'ker (reprGLm rP) by rewrite ker_reprGLm rker_abelem. rewrite -card_quotient ?ker_norm // (card_isog (first_isog _)). apply: leq_trans (dvdn_leq_log _ _ (cardSg (subsetT _))) _ => //. rewrite logn_card_GL_p ?(dim_abelemE abelE) //. by case: logn maxdimE; do 2?case. 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)