proposition: Lemma Zgroup_metacyclic gT (G : {group gT}) : Zgroup G -> metacyclic G.
proof: Proof. elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G; rewrite ltnS => leGn ZgG. have{n IHn leGn} solG: solvable G. have [-> | ntG] := eqsVneq G 1; first apply: solvable1. have [S sylS] := Sylow_exists (pdiv #|G|) G. have cycS: cyclic S := forall_inP ZgG S (p_Sylow sylS). have [H defG] := cyclic_pdiv_normal_complement sylS cycS. have [nsHG _ _ _ _] := sdprod_context defG; rewrite (series_sol nsHG) andbC. rewrite -(isog_sol (sdprod_isog defG)) (abelian_sol (cyclic_abelian cycS)). rewrite metacyclic_sol ?IHn ?(ZgroupS _ ZgG) ?normal_sub //. rewrite (leq_trans _ leGn) // -(sdprod_card defG) ltn_Pmulr // cardG_gt1. by rewrite -rank_gt0 (rank_Sylow sylS) p_rank_gt0 pi_pdiv cardG_gt1. pose K := 'F(G)%G; apply/metacyclicP; exists K. have nsKG: K <| G := Fitting_normal G; have [sKG nKG] := andP nsKG. have cycK: cyclic K by rewrite nil_Zgroup_cyclic ?Fitting_nil ?(ZgroupS sKG). have cKK: abelian K := cyclic_abelian cycK. have{solG cKK} defK: 'C_G(K) = K. by apply/setP/subset_eqP; rewrite cent_sub_Fitting // subsetI sKG. rewrite cycK nil_Zgroup_cyclic ?morphim_Zgroup ?abelian_nil //. rewrite -defK -ker_conj_aut (isog_abelian (first_isog_loc _ _)) //. exact: abelianS (Aut_conj_aut K G) (Aut_cyclic_abelian cycK). 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)