proposition: Lemma trivg_Phi : p.-group P -> ('Phi(P) == 1) = p.-abelem P.
proof: Proof. move=> pP; case: (eqsVneq P 1) => [P1 | ntP]. by rewrite P1 abelem1 -subG1 -P1 Phi_sub. have [p_pr _ _] := pgroup_pdiv pP ntP. apply/eqP/idP=> [trPhi | abP]. apply/abelemP=> //; split=> [|x Px]. apply/commG1P/trivgP; rewrite -trPhi. apply/bigcapsP=> M /predU1P[-> | maxM]; first exact: der1_subG. have /andP[_ nMP]: M <| P := p_maximal_normal pP maxM. rewrite der1_min // cyclic_abelian // prime_cyclic // card_quotient //. by rewrite (p_maximal_index pP). apply/set1gP; rewrite -trPhi; apply/bigcapP=> M. case/predU1P=> [-> | maxM]; first exact: groupX. have /andP[_ nMP] := p_maximal_normal pP maxM. have nMx : x \in 'N(M) by apply: subsetP Px. apply: coset_idr; rewrite ?groupX ?morphX //=; apply/eqP. rewrite -(p_maximal_index pP maxM) -card_quotient // -order_dvdn cardSg //=. by rewrite cycle_subG mem_quotient. apply/trivgP/subsetP=> x Phi_x; rewrite -cycle_subG. have Px: x \in P by apply: (subsetP (Phi_sub P)). have sxP: <[x]> \subset P by rewrite cycle_subG. case/splitsP: (abelem_splits abP sxP) => K /complP[tiKx defP]. have [-> | nt_x] := eqVneq x 1; first by rewrite cycle1. have oxp := abelem_order_p abP Px nt_x. rewrite /= -tiKx subsetI subxx cycle_subG. apply: (bigcapP Phi_x); apply/orP; right. apply: p_index_maximal; rewrite -?divgS -defP ?mulG_subr //. by rewrite (TI_cardMg tiKx) mulnK // [#|_|]oxp. 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)