proposition: Lemma Ohm1_extremal_odd gT (R : {group gT}) p x : p.-group R -> odd #|R| -> ~~ cyclic R -> x \in R -> #|R : <[x]>| = p -> ('Ohm_1(R))%G \in 'E_p^2(R).
proof: Proof. move=> pR oddR ncycR Rx ixR; rewrite -cycle_subG in Rx. have ntR: R :!=: 1 by apply: contra ncycR; move/eqP->; apply: cyclic1. have [p_pr _ [e oR]]:= pgroup_pdiv pR ntR. case p2: (p == 2); first by rewrite oR oddX (eqP p2) in oddR. have [cRR | not_cRR] := orP (orbN (abelian R)). rewrite 2!inE Ohm_sub Ohm1_abelem // -p_rank_abelian //= eqn_leq. rewrite -rank_pgroup // ltnNge -abelian_rank1_cyclic // ncycR andbT. have maxX: maximal <[x]> R by rewrite (p_index_maximal Rx) ?ixR. have nsXR: <[x]> <| R := p_maximal_normal pR maxX. have [_ [y Ry notXy]] := properP (maxgroupp maxX). have defR: <[x]> * <[y]> = R. by apply: mulg_normal_maximal; rewrite ?cycle_subG. rewrite -grank_abelian // -(genGid R) -defR genM_join joing_idl joing_idr. by rewrite (leq_trans (grank_min _)) // cards2 ltnS leq_b1. have{x Rx ixR} [e_gt1 isoR]: 2 < e.+1 /\ R \isog 'Mod_(p ^ e.+1). have:= maximal_cycle_extremal pR not_cRR (cycle_cyclic x) Rx ixR. rewrite p2 orbF /extremal_class oR pfactorKpdiv // pdiv_pfactor //. by do 4!case: andP => //. have [[x y] genR modR] := generators_modular_group p_pr e_gt1 isoR. have [_ _ _ _] := modular_group_structure p_pr e_gt1 genR isoR modR. rewrite xpair_eqE p2; case/(_ 1%N) => // _ oR1. by rewrite 2!inE Ohm_sub oR1 pfactorK ?abelem_Ohm1 ?(card_p2group_abelian p_pr). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)