proposition: Lemma coprime_abel_cent_TI (gT : finGroupType) (A G : {group gT}) : A \subset 'N(G) -> coprime #|G| #|A| -> abelian G -> 'C_[~: G, A](A) = 1.
proof: Proof. move=> nGA coGA abG; pose f x := val (\sum_(a in A) fmod abG x ^@ a)%R. have fM: {in G &, {morph f : x y / x * y}}. move=> x y Gx Gy /=; rewrite -fmvalA -big_split /=; congr (fmval _). by apply: eq_bigr => a Aa; rewrite fmodM // actAr. have nfA x a: a \in A -> f (x ^ a) = f x. move=> Aa; rewrite {2}/f (reindex_inj (mulgI a)) /=; congr (fmval _). apply: eq_big => [b | b Ab]; first by rewrite groupMl. by rewrite -!fmodJ ?groupM ?(subsetP nGA) // conjgM. have kerR: [~: G, A] \subset 'ker (Morphism fM). rewrite gen_subG; apply/subsetP=> xa; case/imset2P=> x a Gx Aa -> {xa}. have Gxa: x ^ a \in G by rewrite memJ_norm ?(subsetP nGA). rewrite commgEl; apply/kerP; rewrite (groupM, morphM) ?(groupV, morphV) //=. by rewrite nfA ?mulVg. apply/trivgP; apply/subsetP=> x /setIP[Rx cAx]; apply/set1P. have Gx: x \in G by apply: subsetP Rx; rewrite commg_subl. rewrite -(expgK coGA Gx) (_ : x ^+ _ = 1) ?expg1n //. rewrite -(fmodK abG Gx) -fmvalZ -(mker (subsetP kerR x Rx)); congr fmval. rewrite -GRing.sumr_const; apply: eq_bigr => a Aa. by rewrite -fmodJ ?(subsetP nGA) // /conjg (centP cAx) // mulKg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)