diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 57 | ||||
| -rw-r--r-- | mathcomp/solvable/alt.v | 61 | ||||
| -rw-r--r-- | mathcomp/solvable/extraspecial.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 10 | ||||
| -rw-r--r-- | mathcomp/solvable/gseries.v | 15 | ||||
| -rw-r--r-- | mathcomp/solvable/hall.v | 21 | ||||
| -rw-r--r-- | mathcomp/solvable/jordanholder.v | 22 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 14 | ||||
| -rw-r--r-- | mathcomp/solvable/nilpotent.v | 12 | ||||
| -rw-r--r-- | mathcomp/solvable/pgroup.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/sylow.v | 7 |
11 files changed, 104 insertions, 121 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 8c2badb..bfdafae 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -1541,12 +1541,13 @@ Implicit Types (p : nat) (G H K E : {group gT}). Lemma abelian_splits x G : x \in G -> #[x] = exponent G -> abelian G -> [splits G, over <[x]>]. Proof. -move=> Gx ox cGG; apply/splitsP; move: {2}_.+1 (ltnSn #|G|) => n. -elim: n gT => // n IHn aT in x G Gx ox cGG *; rewrite ltnS => leGn. +move=> Gx ox cGG; apply/splitsP; have [n] := ubnP #|G|. +elim: n gT => // n IHn aT in x G Gx ox cGG * => /ltnSE-leGn. have: <[x]> \subset G by [rewrite cycle_subG]; rewrite subEproper. -case/predU1P=> [<-|]; first by exists 1%G; rewrite inE -subG1 subsetIr mulg1 /=. -case/properP=> sxG [y]; elim: {y}_.+1 {-2}y (ltnSn #[y]) => // m IHm y. -rewrite ltnS => leym Gy x'y; case: (trivgVpdiv <[y]>) => [y1 | [p p_pr p_dv_y]]. +case/predU1P=> [<- | /properP[sxG [y]]]. + by exists 1%G; rewrite inE -subG1 subsetIr mulg1 /=. +have [m] := ubnP #[y]; elim: m y => // m IHm y /ltnSE-leym Gy x'y. +case: (trivgVpdiv <[y]>) => [y1 | [p p_pr p_dv_y]]. by rewrite -cycle_subG y1 sub1G in x'y. case x_yp: (y ^+ p \in <[x]>); last first. apply: IHm (negbT x_yp); rewrite ?groupX ?(leq_trans _ leym) //. @@ -1558,7 +1559,7 @@ have{x_yp} xp_yp: (y ^+ p \in <[x ^+ p]>). rewrite cycle_subG orderXdiv // divnA // mulnC ox. by rewrite -muln_divA ?dvdn_exponent ?expgM 1?groupX ?cycle_id. have: p <= #[y] by rewrite dvdn_leq. -rewrite leq_eqVlt; case/predU1P=> [{xp_yp m IHm leym}oy | ltpy]; last first. +rewrite leq_eqVlt => /predU1P[{xp_yp m IHm leym}oy | ltpy]; last first. case/cycleP: xp_yp => k; rewrite -expgM mulnC expgM => def_yp. suffices: #[y * x ^- k] < m. by move/IHm; apply; rewrite groupMr // groupV groupX ?cycle_id. @@ -1591,8 +1592,8 @@ Qed. Lemma abelem_splits p G H : p.-abelem G -> H \subset G -> [splits G, over H]. Proof. -elim: {G}_.+1 {-2}G H (ltnSn #|G|) => // m IHm G H. -rewrite ltnS => leGm abelG sHG; case: (eqsVneq H 1) => [-> | ]. +have [m] := ubnP #|G|; elim: m G H => // m IHm G H /ltnSE-leGm abelG sHG. +have [-> | ] := eqsVneq H 1. by apply/splitsP; exists G; rewrite inE mul1g -subG1 subsetIl /=. case/trivgPn=> x Hx ntx; have Gx := subsetP sHG x Hx. have [_ cGG eGp] := and3P abelG. @@ -1630,10 +1631,11 @@ Definition abelian_type (A : {set gT}) := abelian_type_rec #|A| <<A>>. Lemma abelian_type_dvdn_sorted A : sorted [rel m n | n %| m] (abelian_type A). Proof. -set R := SimplRel _; pose G := <<A>>%G. -suffices: path R (exponent G) (abelian_type A) by case: (_ A) => // m t /andP[]. -rewrite /abelian_type -/G; elim: {A}#|A| G {2 3}G (subxx G) => // n IHn G M sGM. -simpl; case: ifP => //= /andP[cGG ntG]; rewrite exponentS ?IHn //=. +set R := SimplRel _; pose G := <<A>>%G; pose M := G. +suffices: path R (exponent M) (abelian_type A) by case: (_ A) => // m t /andP[]. +rewrite /abelian_type -/G; have: G \subset M by []. +elim: {A}#|A| G M => //= n IHn G M sGM. +case: andP => //= -[cGG ntG]; rewrite exponentS ?IHn //=. case: (abelian_type_subproof G) => H /= [//| x _] /dprodP[_ /= <- _ _]. exact: mulG_subr. Qed. @@ -1656,10 +1658,9 @@ Theorem abelian_structure G : abelian G -> {b | \big[dprod/1]_(x <- b) <[x]> = G & map order b = abelian_type G}. Proof. -rewrite /abelian_type genGidG. -elim: {G}#|G| {-2 5}G (leqnn #|G|) => /= [|n IHn] G leGn cGG. - by rewrite leqNgt cardG_gt0 in leGn. -rewrite {1}cGG /=; case: ifP => [ntG|/eqP->]; last first. +rewrite /abelian_type genGidG; have [n] := ubnPleq #|G|. +elim: n G => /= [|n IHn] G leGn cGG; first by rewrite leqNgt cardG_gt0 in leGn. +rewrite [in _ && _]cGG /=; case: ifP => [ntG|/eqP->]; last first. by exists [::]; rewrite ?big_nil. case: (abelian_type_subproof G) => H /= [//|x ox xdefG]; rewrite -ox. have [_ defG cxH tixH] := dprodP xdefG. @@ -1675,7 +1676,7 @@ Lemma count_logn_dprod_cycle p n b G : \big[dprod/1]_(x <- b) <[x]> = G -> count [pred x | logn p #[x] > n] b = logn p #|'Ohm_n.+1(G) : 'Ohm_n(G)|. Proof. -have sOn1 := @Ohm_leq gT _ _ _ (leqnSn n). +have sOn1 H: 'Ohm_n(H) \subset 'Ohm_n.+1(H) by apply: Ohm_leq. pose lnO i (A : {set gT}) := logn p #|'Ohm_i(A)|. have lnO_le H: lnO n H <= lnO n.+1 H. by rewrite dvdn_leq_log ?cardG_gt0 // cardSg ?sOn1. @@ -1781,7 +1782,7 @@ rewrite big_cons => defG; rewrite -(dprod_card defG). rewrite -(dprod_card (Ohm_dprod n defG)) -(dprod_card (Mho_dprod n defG)) /=. rewrite mulnCA -!mulnA mulnCA mulnA; case/dprodP: defG => [[_ H _ defH] _ _ _]. rewrite defH {b G defH IHb}(IHb H defH); congr (_ * _)%N => {H}. -elim: {x}_.+1 {-2}x (ltnSn #[x]) => // m IHm x; rewrite ltnS => lexm. +have [m] := ubnP #[x]; elim: m x => // m IHm x /ltnSE-lexm. case p_x: (p_group <[x]>); last first. case: (eqVneq x 1) p_x => [-> |]; first by rewrite cycle1 p_group1. rewrite -order_gt1 /p_group -orderE; set p := pdiv _ => ntx p'x. @@ -1804,7 +1805,7 @@ set k := logn p #[x]; have ox: #[x] = (p ^ k)%N by rewrite -card_pgroup. case: (leqP k n) => [le_k_n | lt_n_k]. rewrite -(subnKC le_k_n) subnDA subnn expg1 expnD expgM -ox. by rewrite expg_order expg1n order1 muln1. -rewrite !orderXgcd ox -{-3}(subnKC (ltnW lt_n_k)) expnD. +rewrite !orderXgcd ox -[in (p ^ k)%N](subnKC (ltnW lt_n_k)) expnD. rewrite gcdnC gcdnMl gcdnC gcdnMr. by rewrite mulnK ?mulKn ?expn_gt0 ?prime_gt0. Qed. @@ -1823,11 +1824,10 @@ have ->: 'r_p(G) = logn p #|G / K|. rewrite p_rank_abelian // card_quotient /= ?gFnorm // -divgS ?Mho_sub //. by rewrite -(mul_card_Ohm_Mho_abelian 1 cGG) mulnK ?cardG_gt0. case: (grank_witness G) => B genB <-; rewrite -genB. -have: <<B>> \subset G by rewrite genB. -elim: {B genB}_.+1 {-2}B (ltnSn #|B|) => // m IHm B; rewrite ltnS. -case: (set_0Vmem B) => [-> | [x Bx]]. - by rewrite gen0 quotient1 cards1 logn1. -rewrite (cardsD1 x) Bx -{2 3}(setD1K Bx); set B' := B :\ x => ltB'm. +have{genB}: <<B>> \subset G by rewrite genB. +have [m] := ubnP #|B|; elim: m B => // m IHm B. +have [-> | [x Bx]] := set_0Vmem B; first by rewrite gen0 quotient1 cards1 logn1. +rewrite ltnS (cardsD1 x) Bx -[in <<B>>](setD1K Bx); set B' := B :\ x => ltB'm. rewrite -joingE -joing_idl -joing_idr -/<[x]> join_subG => /andP[Gx sB'G]. rewrite cent_joinEl ?(sub_abelian_cent2 cGG) //. have nKx: x \in 'N(K) by rewrite -cycle_subG (subset_trans Gx) ?gFnorm. @@ -1882,10 +1882,11 @@ set e := exponent G => cGG pG /andP[n_gt0 n_lte] eq_Ohm_Mho. suffices: all (pred1 e) (abelian_type G). by rewrite /homocyclic cGG; apply: all_pred1_constant. case/abelian_structure: cGG (abelian_type_gt1 G) => b defG <-. -elim: b {-3}G defG (subxx G) eq_Ohm_Mho => //= x b IHb H. +set H := G in defG eq_Ohm_Mho *; have sHG: H \subset G by []. +elim: b H defG sHG eq_Ohm_Mho => //= x b IHb H. rewrite big_cons => defG; case/dprodP: defG (defG) => [[_ K _ defK]]. -rewrite defK => defHm cxK; rewrite setIC; move/trivgP=> tiKx defHd. -rewrite -{1}defHm {defHm} mulG_subG cycle_subG ltnNge -trivg_card_le1. +rewrite defK => defHm cxK; rewrite setIC => /trivgP-tiKx defHd. +rewrite -{}[in H \subset G]defHm mulG_subG cycle_subG ltnNge -trivg_card_le1. case/andP=> Gx sKG; rewrite -(Mho_dprod _ defHd) => /esym defMho /andP[ntx ntb]. have{defHd} defOhm := Ohm_dprod n defHd. apply/andP; split; last first. @@ -1907,7 +1908,7 @@ rewrite eqn_dvd dvdn_exponent //= -ltnNge => lt_x_e. rewrite (leq_trans (ltn_Pmull (prime_gt1 p_pr) _)) ?expn_gt0 ?prime_gt0 //. rewrite -expnS dvdn_leq // ?gcdn_gt0 ?order_gt0 // dvdn_gcd. rewrite pfactor_dvdn // dvdn_exp2l. - by rewrite -{2}[logn p _]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x. + by rewrite -[xp in _ < xp]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x. rewrite ltn_sub2r // ltnNge -(dvdn_Pexp2l _ _ (prime_gt1 p_pr)) -!p_part. by rewrite !part_pnat_id // (pnat_dvd (exponent_dvdn G)). Qed. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index d6ada5f..cb86051 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -329,47 +329,32 @@ Lemma rfd_odd (p : {perm T}) : p x = x -> rfd p = p :> bool. Proof. have rfd1: rfd 1 = 1. by apply/permP => u; apply: val_inj; rewrite permE /= if_same !perm1. -have HP0 (t : {perm T}): #|[set x | t x != x]| = 0 -> rfd t = t :> bool. -- move=> Ht; suff ->: t = 1 by rewrite rfd1 !odd_perm1. - apply/permP => z; rewrite perm1; apply/eqP/wlog_neg => nonfix_z. - by rewrite (cardD1 z) inE nonfix_z in Ht. -elim: #|_| {-2}p (leqnn #|[set x | p x != x]|) => {p}[|n Hrec] p Hp Hpx. - by apply: HP0; move: Hp; case: card. -case Ex: (pred0b (mem [set x | p x != x])); first by apply: HP0; move/eqnP: Ex. -case/pred0Pn: Ex => x1; rewrite /= inE => Hx1. -have nx1x: x1 != x by apply/eqP => HH; rewrite HH Hpx eqxx in Hx1. -have npxx1: p x != x1 by apply/eqP => HH; rewrite -HH !Hpx eqxx in Hx1. -have npx1x: p x1 != x. - by apply/eqP; rewrite -Hpx; move/perm_inj => HH; case/eqP: nx1x. +have [n] := ubnP #|[set x | p x != x]|; elim: n p => // n IHn p le_p_n px_x. +have [p_id | [x1 Hx1]] := set_0Vmem [set x | p x != x]. + suffices ->: p = 1 by rewrite rfd1 !odd_perm1. + by apply/permP => z; apply: contraFeq (in_set0 z); rewrite perm1 -p_id inE. +have nx1x: x1 != x by apply: contraTneq Hx1 => ->; rewrite inE px_x eqxx. +have npxx1: p x != x1 by apply: contraNneq nx1x => <-; rewrite px_x. +have npx1x: p x1 != x by rewrite -px_x (inj_eq perm_inj). pose p1 := p * tperm x1 (p x1). -have Hp1: p1 x = x. - by rewrite /p1 permM; case tpermP => // [<-|]; [rewrite Hpx | move/perm_inj]. -have Hcp1: #|[set x | p1 x != x]| <= n. - have F1 y: p y = y -> p1 y = y. - move=> Hy; rewrite /p1 permM Hy. - by case: tpermP => [<-|/(canLR (permK p))<-|] //; apply/(canLR (permK p)). - have F2: p1 x1 = x1 by rewrite /p1 permM tpermR. - have F3: [set x | p1 x != x] \subset [predD1 [set x | p x != x] & x1]. - apply/subsetP => z; rewrite !inE permM. - case tpermP => HH1 HH2. - - rewrite eq_sym HH1 andbb; apply/eqP=> dx1. - by rewrite dx1 HH1 dx1 eqxx in HH2. - - by rewrite (perm_inj HH1) eqxx in HH2. - by move->; rewrite andbT; apply/eqP => HH3; rewrite HH3 in HH2. - apply: (leq_trans (subset_leq_card F3)). - by move: Hp; rewrite (cardD1 x1) inE Hx1. -have ->: p = p1 * tperm x1 (p x1) by rewrite -mulgA tperm2 mulg1. -rewrite odd_permM odd_tperm eq_sym Hx1 morphM; last 2 first. -- by rewrite 2!inE; apply/astab1P. -- by rewrite 2!inE; apply/astab1P; rewrite -{1}Hpx /= /aperm -permM. -rewrite odd_permM Hrec //=; congr (_ (+) _). +have fix_p1 y: p y = y -> p1 y = y. + by move=> pyy; rewrite permM; have [<-|/perm_inj<-|] := tpermP; rewrite ?pyy. +have p1x_x: p1 x = x by apply: fix_p1. +have{le_p_n} lt_p1_n: #|[set x | p1 x != x]| < n. + move: le_p_n; rewrite ltnS (cardsD1 x1) Hx1; apply/leq_trans/subset_leq_card. + rewrite subsetD1 inE permM tpermR eqxx andbT. + by apply/subsetP=> y; rewrite !inE; apply: contraNneq=> /fix_p1->. +transitivity (p1 (+) true); last first. + by rewrite odd_permM odd_tperm -Hx1 inE eq_sym addbK. +have ->: p = p1 * tperm x1 (p x1) by rewrite -tpermV mulgK. +rewrite morphM; last 2 first; first by rewrite 2!inE; apply/astab1P. + by rewrite 2!inE; apply/astab1P; rewrite -[RHS]p1x_x permM px_x. +rewrite odd_permM IHn //=; congr (_ (+) _). pose x2 : T' := Sub x1 nx1x; pose px2 : T' := Sub (p x1) npx1x. -suff ->: rfd (tperm x1 (p x1)) = tperm x2 px2. - by rewrite odd_tperm -val_eqE eq_sym. +suffices ->: rfd (tperm x1 (p x1)) = tperm x2 px2. + by rewrite odd_tperm eq_sym; rewrite inE in Hx1. apply/permP => z; apply/val_eqP; rewrite permE /= tpermD // eqxx. -case: (tpermP x2) => [->|->|HH1 HH2]; rewrite /x2 ?tpermL ?tpermR 1?tpermD //. - by apply/eqP=> HH3; case: HH1; apply: val_inj. -by apply/eqP => HH3; case: HH2; apply: val_inj. +by rewrite !permE /= -!val_eqE /= !(fun_if sval) /=. Qed. Lemma rfd_iso : 'C_('Alt_T)[x | 'P] \isog 'Alt_T'. diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 0aacd7c..58c3cf0 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -420,7 +420,7 @@ have iC1U (U : {group gT}) x: by rewrite -norm_joinEl ?cardSg ?join_subG ?(subset_trans sUG). have oCG (U : {group gT}): Z \subset U -> U \subset G -> #|'C_G(U)| = (p * #|G : U|)%N. -- elim: {U}_.+1 {-2}U (ltnSn #|U|) => // m IHm U leUm sZU sUG. +- have [m] := ubnP #|U|; elim: m U => // m IHm U leUm sZU sUG. have [<- | neZU] := eqVneq Z U. by rewrite -oZ Lagrange // (setIidPl _) // centsC subsetIr. have{neZU} [x Gx not_cUx]: exists2 x, x \in G & x \notin 'C(U). diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index be885b1..36c4d12 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -575,9 +575,9 @@ suffices{k k_gt0 le_k_n2} defGn2: <[x ^+ p]> \x <[y]> = 'Ohm_(n.-2)(G). rewrite -subSn // -subSS def_n1 def_n => -> /=; rewrite subnSK // subn2. by apply/eqP; rewrite eqEsubset OhmS ?Ohm_sub //= -{1}Ohm_id OhmS ?Ohm_leq. rewrite dprodEY //=; last by apply/trivgP; rewrite -tiXY setSI ?cycleX. -apply/eqP; rewrite eqEsubset join_subG !cycle_subG /= {-2}(OhmE _ pG) -/r. -rewrite def_n (subsetP (Ohm_leq G (ltn0Sn _))) // mem_gen /=; last first. - by rewrite !inE -order_dvdn oxp groupX /=. +apply/eqP; rewrite eqEsubset join_subG !cycle_subG /= [in y \in _]def_n. +rewrite (subsetP (Ohm_leq G (ltn0Sn _)) y) //= (OhmE _ pG) -/r. +rewrite mem_gen /=; last by rewrite !inE -order_dvdn oxp groupX /=. rewrite gen_subG /= cent_joinEr // -defXY; apply/subsetP=> uv; case/setIP. case/imset2P=> u v Xu Yv ->{uv}; rewrite /r inE def_n expnS expgM. case/lcosetP: (XYp u v Xu Yv) => _ /cycleP[j ->] ->. @@ -786,8 +786,8 @@ have defK: K = [set w]. apply/eqP; rewrite eqEsubset sub1set Kw andbT subDset setUC. apply/subsetP=> uivj; have: uivj \in B by rewrite inE. rewrite -{1}defB => /imset2P[_ _ /cycleP[i ->] /cycleP[j ->] ->] {uivj}. - rewrite !inE sqrB -{-1}[j]odd_double_half. - case: (odd j); rewrite -order_dvdn ?ov // ou -def2r -mul2n dvdn_pmul2l //. + rewrite !inE sqrB; set b := odd j; rewrite -[j]odd_double_half -/b. + case: b; rewrite -order_dvdn ?ov // ou -def2r -mul2n dvdn_pmul2l //. case/dvdnP=> k ->{i}; apply/orP. rewrite add0n -[j./2]odd_double_half addnC doubleD -!muln2 -mulnA. rewrite -(expg_mod_order v) ov modnMDl; case: (odd _); last first. diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 28ca208..a96295f 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -116,7 +116,7 @@ Lemma subnormalP H G : reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G). Proof. apply: (iffP andP) => [[sHG snHG] | [s Hsn <-{G}]]. - elim: {G}#|G| {-2}G sHG snHG => [|m IHm] G sHG. + move: #|G| snHG => m; elim: m => [|m IHm] in G sHG *. by exists [::]; last by apply/eqP; rewrite eq_sym. rewrite iterSr => /IHm[|s Hsn defG]. by rewrite sub_gen // class_supportEr (bigD1 1) //= conjsg1 subsetUl. @@ -125,10 +125,10 @@ apply: (iffP andP) => [[sHG snHG] | [s Hsn <-{G}]]. by rewrite norms_gen ?class_support_norm. set f := fun _ => <<_>>; have idf: iter _ f H == H. by elim=> //= m IHm; rewrite (eqP IHm) /f class_support_id genGid. -elim: {s}(size s) {-2}s (eqxx (size s)) Hsn => [[] //= | m IHm s]. -case/lastP: s => // s G; rewrite size_rcons last_rcons -cats1 cat_path /=. -set K := last H s => def_m /and3P[Hsn /andP[sKG nKG] _]. -have:= sKG; rewrite subEproper; case/predU1P=> [<-|prKG]; first exact: IHm. +have [m] := ubnP (size s); elim: m s Hsn => // m IHm /lastP[//|s G]. +rewrite size_rcons last_rcons rcons_path /= ltnS. +set K := last H s => /andP[Hsn /andP[sKG nKG]] lt_s_m. +have:= sKG; rewrite subEproper => /predU1P[<-|prKG]; first exact: IHm. pose L := [group of f G]. have sHK: H \subset K by case/IHm: Hsn. have sLK: L \subset K by rewrite gen_subG class_support_sub_norm. @@ -136,7 +136,8 @@ rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iter_add iterSr. have defH: H = setIgr L H by rewrite -sub_setIgr ?sub_gen ?sub_class_support. have: normal.-series H (map (setIgr L) s) by rewrite defH path_setIgr. case/IHm=> [|_]; first by rewrite size_map. -by rewrite {1 2}defH last_map (subset_trans sHK) //= (setIidPr sLK) => /eqP->. +rewrite [in last _]defH last_map (subset_trans sHK) //=. +by rewrite (setIidPr sLK) => /eqP->. Qed. Lemma subnormal_refl G : G <|<| G. @@ -513,7 +514,7 @@ Qed. Lemma chief_series_exists H G : H <| G -> {s | (G.-chief).-series 1%G s & last 1%G s = H}. Proof. -elim: {H}_.+1 {-2}H (ltnSn #|H|) => // m IHm U leUm nsUG. +have [m] := ubnP #|H|; elim: m H => // m IHm U leUm nsUG. have [-> | ntU] := eqVneq U 1%G; first by exists [::]. have [V maxV]: {V : {group gT} | maxnormal V U G}. by apply: ex_maxgroup; exists 1%G; rewrite proper1G ntU norms1. diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index 43e429f..6234224 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.v @@ -31,8 +31,8 @@ Implicit Type gT : finGroupType. Theorem SchurZassenhaus_split gT (G H : {group gT}) : Hall G H -> H <| G -> [splits G, over H]. Proof. -move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in gT G H *. -rewrite ltnS => Gn hallH nsHG; have [sHG nHG] := andP nsHG. +have [n] := ubnP #|G|; elim: n => // n IHn in gT G H * => /ltnSE-Gn hallH nsHG. +have [sHG nHG] := andP nsHG. have [-> | [p pr_p pH]] := trivgVpdiv H. by apply/splitsP; exists G; rewrite inE -subG1 subsetIl mul1g eqxx. have [P sylP] := Sylow_exists p H. @@ -102,8 +102,9 @@ Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) : coprime #|H| #|K| -> #|K1| = #|K| -> exists2 x, x \in H & K1 :=: K :^ x. Proof. -move: {2}_.+1 (ltnSn #|H|) => n; elim: n => // n IHn in gT H K K1 *. -rewrite ltnS => leHn solH nHK; have [-> | ] := eqsVneq H 1. +have [n] := ubnP #|H|. +elim: n => // n IHn in gT H K K1 * => /ltnSE-leHn solH nHK. +have [-> | ] := eqsVneq H 1. rewrite mul1g => sK1K _ eqK1K; exists 1; first exact: set11. by apply/eqP; rewrite conjsg1 eqEcard sK1K eqK1K /=. pose G := (H <*> K)%G. @@ -150,9 +151,8 @@ Lemma SchurZassenhaus_trans_actsol gT (G A B : {group gT}) : coprime #|G| #|A| -> #|A| = #|B| -> exists2 x, x \in G & B :=: A :^ x. Proof. -set AG := A <*> G; move: {2}_.+1 (ltnSn #|AG|) => n. -elim: n => // n IHn in gT A B G AG *. -rewrite ltnS => leAn solA nGA sB_AG coGA oAB. +set AG := A <*> G; have [n] := ubnP #|AG|. +elim: n => // n IHn in gT A B G AG * => /ltnSE-leAn solA nGA sB_AG coGA oAB. have [A1 | ntA] := eqsVneq A 1. by exists 1; rewrite // conjsg1 A1 (@card1_trivg _ B) // -oAB A1 cards1. have [M [sMA nsMA ntM]] := solvable_norm_abelem solA (normal_refl A) ntA. @@ -218,8 +218,7 @@ Lemma Hall_exists_subJ pi gT (G : {group gT}) : & forall K : {group gT}, K \subset G -> pi.-group K -> exists2 x, x \in G & K \subset H :^ x. Proof. -move: {2}_.+1 (ltnSn #|G|) => n. -elim: n gT G => // n IHn gT G; rewrite ltnS => leGn solG. +have [n] := ubnP #|G|; elim: n gT G => // n IHn gT G /ltnSE-leGn solG. have [-> | ntG] := eqsVneq G 1. exists 1%G => [|_ /trivGP-> _]; last by exists 1; rewrite ?set11 ?sub1G. by rewrite pHallE sub1G cards1 part_p'nat. @@ -581,8 +580,8 @@ Proposition coprime_Hall_subset pi (gT : finGroupType) (A G X : {group gT}) : X \subset G -> pi.-group X -> A \subset 'N(X) -> exists H : {group gT}, [/\ pi.-Hall(G) H, A \subset 'N(H) & X \subset H]. Proof. -move: {2}_.+1 (ltnSn #|G|) => n. -elim: n => // n IHn in gT A G X * => leGn nGA coGA solG sXG piX nXA. +have [n] := ubnP #|G|. +elim: n => // n IHn in gT A G X * => /ltnSE-leGn nGA coGA solG sXG piX nXA. have [G1 | ntG] := eqsVneq G 1. case: (coprime_Hall_exists pi nGA) => // H hallH nHA. by exists H; split; rewrite // (subset_trans sXG) // G1 sub1G. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index d191e20..3d3162b 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -174,8 +174,7 @@ Qed. Lemma JordanHolderUniqueness (G : gTg) (s1 s2 : seq gTg) : comps G s1 -> comps G s2 -> perm_eq (mkfactors G s1) (mkfactors G s2). Proof. -elim: {G}#|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => cs1 cs2. - by rewrite leqNgt cardG_gt0 in cG. +have [n] := ubnP #|G|; elim: n G => // n Hi G in s1 s2 * => /ltnSE-cG cs1 cs2. have [G1 | ntG] := boolP (G :==: 1). have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2). @@ -188,10 +187,10 @@ case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}. by move: (trivg_comps cs2); rewrite eqxx; move/negP:ntG. case/andP: cs1 => /= lst1; case/andP=> maxN_1 pst1. case/andP: cs2 => /= lst2; case/andP=> maxN_2 pst2. -have cN1 : #|N1| <= n. - by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_1). -have cN2 : #|N2| <= n. - by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_2). +have cN1 : #|N1| < n. + by rewrite (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_1). +have cN2 : #|N2| < n. + by rewrite (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_2). case: (N1 =P N2) {s2 es2} => [eN12 |]. by rewrite eN12 /= perm_cons Hi // /comps ?lst2 //= -eN12 lst1. move/eqP; rewrite -val_eqE /=; move/eqP=> neN12. @@ -588,8 +587,7 @@ Lemma StrongJordanHolderUniqueness (G : {group rT}) (s1 s2 : seq {group rT}) : G \subset D -> acomps to G s1 -> acomps to G s2 -> perm_eq (mkfactors G s1) (mkfactors G s2). Proof. -elim: {G} #|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => hsD cs1 cs2. - by rewrite leqNgt cardG_gt0 in cG. +have [n] := ubnP #|G|; elim: n G => // n Hi G in s1 s2 * => cG hsD cs1 cs2. case/orP: (orbN (G :==: 1)) => [tG | ntG]. have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2). @@ -608,10 +606,10 @@ have sN1D : N1 \subset D. by apply: subset_trans hsD; apply: maxainv_sub maxN_1. have sN2D : N2 \subset D. by apply: subset_trans hsD; apply: maxainv_sub maxN_2. -have cN1 : #|N1| <= n. - by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxainv_proper maxN_1). -have cN2 : #|N2| <= n. - by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxainv_proper maxN_2). +have cN1 : #|N1| < n. + by rewrite -ltnS (leq_trans _ cG) ?ltnS ?proper_card ?(maxainv_proper maxN_1). +have cN2 : #|N2| < n. + by rewrite -ltnS (leq_trans _ cG) ?ltnS ?proper_card ?(maxainv_proper maxN_2). case: (N1 =P N2) {s2 es2} => [eN12 |]. by rewrite eN12 /= perm_cons Hi // /acomps ?lst2 //= -eN12 lst1. move/eqP; rewrite -val_eqE /=; move/eqP=> neN12. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 0dfb4d1..95b7184 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -993,7 +993,7 @@ Lemma card_subcent_extraspecial U : U \subset G -> #|'C_G(U)| = (#|'Z(G) :&: U| * #|G : U|)%N. Proof. move=> sUG; rewrite setIAC (setIidPr sUG). -elim: {U}_.+1 {-2}U (ltnSn #|U|) sUG => // m IHm U leUm sUG. +have [m leUm] := ubnP #|U|; elim: m => // m IHm in U leUm sUG *. have [cUG | not_cUG]:= orP (orbN (G \subset 'C(U))). by rewrite !(setIidPl _) ?Lagrange // centsC. have{not_cUG} [x Gx not_cUx] := subsetPn not_cUG. @@ -1183,7 +1183,7 @@ Theorem extraspecial_structure S : p.-group S -> extraspecial S -> {Es | all (fun E => (#|E| == p ^ 3)%N && ('Z(E) == 'Z(S))) Es & \big[cprod/1%g]_(E <- Es) E \* 'Z(S) = S}. Proof. -elim: {S}_.+1 {-2}S (ltnSn #|S|) => // m IHm S leSm pS esS. +have [m] := ubnP #|S|; elim: m S => // m IHm S leSm pS esS. have [x Z'x]: {x | x \in S :\: 'Z(S)}. apply/sigW/set0Pn; rewrite -subset0 subDset setU0. apply: contra (extraspecial_nonabelian esS) => sSZ. @@ -1210,11 +1210,11 @@ Let oZ := card_center_extraspecial pS esS. (* This is Aschbacher (23.10)(2). *) Lemma card_extraspecial : {n | n > 0 & #|S| = (p ^ n.*2.+1)%N}. Proof. -exists (logn p #|S|)./2. +set T := S; exists (logn p #|T|)./2. rewrite half_gt0 ltnW // -(leq_exp2l _ _ (prime_gt1 p_pr)) -card_pgroup //. exact: min_card_extraspecial. -have [Es] := extraspecial_structure pS esS. -elim: Es {3 4 5}S => [_ _ <-| E s IHs T] /=. +have [Es] := extraspecial_structure pS esS; rewrite -[in RHS]/T. +elim: Es T => [_ _ <-| E s IHs T] /=. by rewrite big_nil cprod1g oZ (pfactorK 1). rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oEp3; move/eqP=> defZE. move/IHs=> {IHs}IHs; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU. @@ -1233,8 +1233,8 @@ have [Es] := extraspecial_structure pS esS. elim: Es S oZ => [T _ _ <-| E s IHs T oZT] /=. rewrite big_nil cprod1g (center_idP (center_abelian T)). by apply/Aut_sub_fullP=> // g injg gZ; exists g. -rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oE; move/eqP=> defZE. -move=> es_s; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU. +rewrite -andbA big_cons -cprodA => /and3P[/eqP-oE /eqP-defZE es_s]. +case/cprodP=> -[_ U _ defU]; rewrite defU => defT cEU. have sUT: U \subset T by rewrite -defT mulG_subr. have sZU: 'Z(T) \subset U. by case/cprodP: defU => [[V _ -> _] <- _]; apply: mulG_subr. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index f0448d7..06f3152 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -238,8 +238,8 @@ apply/idP/mapP=> {s}/= [nilG | [n _ Ln1]]; last first. rewrite -subG1 {}Ln1; elim: n => // n IHn. by rewrite (subset_trans sHR) ?commSg. pose m := #|G|.-1; exists m; first by rewrite mem_iota /= prednK. -rewrite ['L__(G)]card_le1_trivg //= -(subnn m). -elim: {-2}m => [|n]; [by rewrite subn0 prednK | rewrite lcnSn subnS]. +set n := m; rewrite ['L__(G)]card_le1_trivg //= -(subnn m) -[m in _ - m]/n. +elim: n => [|n]; [by rewrite subn0 prednK | rewrite lcnSn subnS]. case: (eqsVneq 'L_n.+1(G) 1) => [-> | ntLn]; first by rewrite comm1G cards1. case: (m - n) => [|m' /= IHn]; first by rewrite leqNgt cardG_gt1 ntLn. rewrite -ltnS (leq_trans (proper_card _) IHn) //. @@ -464,8 +464,8 @@ Qed. Lemma ucn_lcnP n G : ('L_n.+1(G) == 1) = ('Z_n(G) == G). Proof. -rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G). -elim: {1 3}n 0 (addn0 n) => [j <- //|i IHi j]. +rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G); set i := (n in LHS). +have: i + 0 = n by [rewrite addn0]; elim: i 0 => [j <- //|i IHi j]. rewrite addSnnS => /IHi <- {IHi}; rewrite ucnSn lcnSn. rewrite -sub_morphim_pre ?gFsub_trans ?gFnorm_trans // subsetI. by rewrite morphimS ?gFsub // quotient_cents2 ?gFsub_trans ?gFnorm_trans. @@ -611,8 +611,8 @@ Qed. Lemma nilpotent_subnormal G H : nilpotent G -> H \subset G -> H <|<| G. Proof. -move=> nilG; elim: {H}_.+1 {-2}H (ltnSn (#|G| - #|H|)) => // m IHm H. -rewrite ltnS => leGHm sHG. +move=> nilG; have [m] := ubnP (#|G| - #|H|). +elim: m H => // m IHm H /ltnSE-leGHm sHG. have [->|] := eqVproper sHG; first exact: subnormal_refl. move/(nilpotent_proper_norm nilG); set K := 'N_G(H) => prHK. have snHK: H <|<| K by rewrite normal_subnormal ?normalSG. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index 5c572b7..2ed68f0 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -623,8 +623,8 @@ Proof. by rewrite /psubgroup sub1G pgroup1. Qed. Lemma Cauchy p G : prime p -> p %| #|G| -> {x | x \in G & #[x] = p}. Proof. -move=> p_pr; elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G. -rewrite ltnS => leGn pG; pose xpG := [pred x in G | #[x] == p]. +move=> p_pr; have [n] := ubnP #|G|; elim: n G => // n IHn G /ltnSE-leGn pG. +pose xpG := [pred x in G | #[x] == p]. have [x /andP[Gx /eqP] | no_x] := pickP xpG; first by exists x. have{pG n leGn IHn} pZ: p %| #|'C_G(G)|. suffices /dvdn_addl <-: p %| #|G :\: 'C(G)| by rewrite cardsID. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index 2a46564..f3ecae2 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -514,7 +514,7 @@ Qed. Lemma nil_Zgroup_cyclic G : Zgroup G -> nilpotent G -> cyclic G. Proof. -elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G; rewrite ltnS => leGn ZgG nilG. +have [n] := ubnP #|G|; elim: n G => // n IHn G /ltnSE-leGn ZgG nilG. have [->|[p pr_p pG]] := trivgVpdiv G; first by rewrite -cycle1 cycle_cyclic. have /dprodP[_ defG Cpp' _] := nilpotent_pcoreC p nilG. have /cyclicP[x def_p]: cyclic 'O_p(G). @@ -567,9 +567,8 @@ Theorem Baer_Suzuki x G : x \in G -> (forall y, y \in G -> p.-group <<[set x; x ^ y]>>) -> x \in 'O_p(G). Proof. -elim: {G}_.+1 {-2}G x (ltnSn #|G|) => // n IHn G x; rewrite ltnS. -set E := x ^: G => leGn Gx pE. -have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. +have [n] := ubnP #|G|; elim: n G x => // n IHn G x /ltnSE-leGn Gx pE. +set E := x ^: G; have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. move=> _ _ /imsetP[y1 Gy1 ->] /imsetP[y2 Gy2 ->]. rewrite -(mulgKV y1 y2) conjgM -2!conjg_set1 -conjUg genJ pgroupJ. by rewrite pE // groupMl ?groupV. |