proposition: Lemma center_special_abelem : p.-group G -> special G -> p.-abelem 'Z(G).
proof: Proof. move=> pG [defPhi defG']. have [-> | ntG] := eqsVneq G 1; first by rewrite center1 abelem1. have [p_pr _ _] := pgroup_pdiv pG ntG. have fM: {in 'Z(G) &, {morph expgn^~ p : x y / x * y}}. by move=> x y /setIP[_ /centP cxG] /setIP[/cxG cxy _]; apply: expgMn. rewrite abelemE //= center_abelian; apply/exponentP=> /= z Zz. apply: (@kerP _ _ _ (Morphism fM)) => //; apply: subsetP z Zz. rewrite -{1}defG' gen_subG; apply/subsetP=> _ /imset2P[x y Gx Gy ->]. have Zxy: [~ x, y] \in 'Z(G) by rewrite -defG' mem_commg. have Zxp: x ^+ p \in 'Z(G). rewrite -defPhi (Phi_joing pG) (MhoE 1 pG) joing_idr mem_gen // !inE. by rewrite expn1 orbC (imset_f (expgn^~ p)). rewrite mem_morphpre /= ?defG' ?Zxy // inE -commXg; last first. by red; case/setIP: Zxy => _ /centP->. by apply/commgP; red; case/setIP: Zxp => _ /centP->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)