proposition: Lemma pi_center_nilpotent G : nilpotent G -> \pi('Z(G)) = \pi(G).
proof: Proof. move=> nilG; apply/eq_piP => /= p. apply/idP/idP=> [|pG]; first exact: (piSg (center_sub _)). move: (pG); rewrite !mem_primes !cardG_gt0; case/andP=> p_pr _. pose Z := 'O_p(G) :&: 'Z(G); have ntZ: Z != 1. rewrite meet_center_nil ?pcore_normal // trivg_card_le1 -ltnNge. rewrite (card_Hall (nilpotent_pcore_Hall p nilG)) p_part. by rewrite (ltn_exp2l 0 _ (prime_gt1 p_pr)) logn_gt0. have pZ: p.-group Z := pgroupS (subsetIl _ _) (pcore_pgroup _ _). have{ntZ pZ} [_ pZ _] := pgroup_pdiv pZ ntZ. by rewrite p_pr (dvdn_trans pZ) // cardSg ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)