proposition: Proposition exponent_Ohm1_rank2 gT p (R : {group gT}) : p.-group R -> 'r(R) <= 2 -> p > 3 -> exponent 'Ohm_1(R) %| p.
proof: Proof. move=> pR rR p_gt3; wlog p_pr: / prime p. have [-> | ntR] := eqsVneq R 1; first by rewrite Ohm1 exponent1 dvd1n. by apply; have [->] := pgroup_pdiv pR ntR. wlog minR: R pR rR / forall S, gval S \proper R -> exponent 'Ohm_1(S) %| p. elim: {R}_.+1 {-2}R (ltnSn #|R|) => // m IHm R leRm in pR rR * => IH. apply: (IH) => // S; rewrite properEcard; case/andP=> sSR ltSR. exact: IHm (leq_trans ltSR _) (pgroupS sSR pR) (leq_trans (rankS sSR) rR) IH. wlog not_clR_le3: / ~~ (nil_class R <= 3). case: leqP => [clR_le3 _ | _ -> //]. have [||-> //] := exponent_odd_nil23 pR; last by rewrite p_gt3. by apply: odd_pgroup_odd pR; case/even_prime: p_pr p_gt3 => ->. rewrite -sub_LdivT (OhmE 1 pR) gen_set_id ?subsetIr //. apply/group_setP; rewrite !inE group1 expg1n. split=> //= x y; case/LdivP=> Rx xp1; case/LdivP=> Ry yp1. rewrite !inE groupM //=; apply: contraR not_clR_le3 => nt_xyp. pose XY := <[x]> <*> <[y]>. have [XYx XYy]: x \in XY /\ y \in XY by rewrite -!cycle_subG; apply/joing_subP. have{nt_xyp} defR: XY = R. have sXY_R : XY \subset R by rewrite join_subG !cycle_subG Rx Ry. have pXY := pgroupS sXY_R pR; have [// | ltXY_R] := eqVproper sXY_R. rewrite (exponentP (minR _ ltXY_R)) ?eqxx // in nt_xyp. by rewrite (OhmE 1 pXY) groupM ?mem_gen ?inE ?XYx ?XYy /= ?xp1 ?yp1. have sXR: <[x]> \subset R by rewrite cycle_subG. have [<- | ltXR] := eqVproper sXR. by rewrite 2?leqW // nil_class1 cycle_abelian. have [S maxS sXS]: {S : {group gT} | maximal S R & <[x]> \subset S}. exact: maxgroup_exists. have nsSR: S <| R := p_maximal_normal pR maxS; have [sSR _] := andP nsSR. have{nsSR} nsS1R: 'Ohm_1(S) <| R := gFnormal_trans _ nsSR. have [sS1R nS1R] := andP nsS1R; have pS1 := pgroupS sS1R pR. have expS1p: exponent 'Ohm_1(S) %| p := minR S (maxgroupp maxS). have{expS1p} dimS1: logn p #|'Ohm_1(S)| <= 3. exact: rank2_exponent_p_p3group pS1 (leq_trans (rankS sS1R) rR) expS1p. have sXS1: <[x]> \subset 'Ohm_1(S). rewrite cycle_subG /= (OhmE 1 (pgroupS sSR pR)) mem_gen //. by rewrite !inE -cycle_subG sXS xp1 /=. have dimS1b: logn p #|R / 'Ohm_1(S)| <= 1. rewrite -quotientYidl // -defR joingA (joing_idPl sXS1). rewrite quotientYidl ?cycle_subG ?(subsetP nS1R) //. rewrite (leq_trans (logn_quotient _ _ _)) // -(pfactorK 1 p_pr). by rewrite dvdn_leq_log ?prime_gt0 // order_dvdn yp1. rewrite (leq_trans (nil_class_pgroup pR)) // geq_max /= -subn1 leq_subLR. by rewrite -(Lagrange sS1R) lognM // -card_quotient // addnC leq_add. 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)