diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 6 | ||||
| -rw-r--r-- | mathcomp/solvable/alt.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 176 | ||||
| -rw-r--r-- | mathcomp/solvable/center.v | 6 | ||||
| -rw-r--r-- | mathcomp/solvable/commutator.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/extraspecial.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 18 | ||||
| -rw-r--r-- | mathcomp/solvable/finmodule.v | 18 | ||||
| -rw-r--r-- | mathcomp/solvable/frobenius.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/gfunctor.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/gseries.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/hall.v | 6 | ||||
| -rw-r--r-- | mathcomp/solvable/jordanholder.v | 8 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 26 | ||||
| -rw-r--r-- | mathcomp/solvable/nilpotent.v | 8 | ||||
| -rw-r--r-- | mathcomp/solvable/pgroup.v | 6 | ||||
| -rw-r--r-- | mathcomp/solvable/sylow.v | 8 |
18 files changed, 155 insertions, 155 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index d6dac93..2b0ab00 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -176,7 +176,7 @@ Qed. Lemma OhmPredP (x : gT) : reflect (exists2 p, prime p & x ^+ (p ^ n) = 1) (x ^+ (pdiv #[x] ^ n) == 1). Proof. -have [-> | nt_x] := eqVneq x 1. +have [-> | nt_x] := eqVneq x 1. by rewrite expg1n eqxx; left; exists 2; rewrite ?expg1n. apply: (iffP idP) => [/eqP | [p p_pr /eqP x_pn]]. by exists (pdiv #[x]); rewrite ?pdiv_prime ?order_gt1. @@ -702,7 +702,7 @@ move=> p_pr; apply: (iffP (pmaxElemP p G E)) => [[] | defE]. by rewrite cycle_abelem ?p_pr ?orbT // order_dvdn xp. by rewrite (subsetP sEG) // (subsetP cEE) // (exponentP eE). split=> [|H]; last first. - case/pElemP=> sHG /abelemP[// | cHH Hp1] sEH. + case/pElemP=> sHG /abelemP[// | cHH Hp1] sEH. apply/eqP; rewrite eqEsubset sEH andbC /= -defE; apply/subsetP=> x Hx. by rewrite 3!inE (subsetP sHG) // Hp1 ?(subsetP (centsS _ cHH)) /=. apply/pElemP; split; first by rewrite -defE -setIA subsetIl. @@ -1891,7 +1891,7 @@ 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. case/andP=> Gx sKG; rewrite -(Mho_dprod _ defHd) => /esym defMho /andP[ntx ntb]. -have{defHd} defOhm := Ohm_dprod n defHd. +have{defHd} defOhm := Ohm_dprod n defHd. apply/andP; split; last first. apply: (IHb K) => //; have:= dprod_modr defMho (Mho_sub _ _). rewrite -(dprod_modr defOhm (Ohm_sub _ _)). diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index baf4792..73a3b1b 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -271,7 +271,7 @@ have nSyl5: #|'Syl_5(H)| = 1%N. move: (card_Syl_dvd 5 H) (card_Syl_mod H prime_5). rewrite Hcard20; case: (card _) => // n Hdiv. move: (dvdn_leq (isT: (0 < 20)%N) Hdiv). - by move: (n) Hdiv; do 20 (case => //). + by move: (n) Hdiv; do 20 (case=> //). case: (Sylow_exists 5 H) => S; case/pHallP=> sSH oS. have{oS} oS: #|S| = 5 by rewrite oS p_part Hcard20. suff: 20 %| #|S| by rewrite oS. @@ -350,7 +350,7 @@ have Hp1: p1 x = x. have Hcp1: #|[set x | p1 x != x]| <= n. have F1 y: p y = y -> p1 y = y. move=> Hy; rewrite /p1 permM Hy. - case tpermP => //; first by move => <-. + case tpermP => //; first by move=> <-. by move=> Hpx1; apply: (@perm_inj _ p); rewrite -Hpx1. 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]. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 638276c..d602d0a 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -79,13 +79,13 @@ Ltac inj_tac := end. Lemma R1_inj : injective R1. -Proof. by inj_tac; repeat (destruct val => //=; first by apply /eqP). Qed. +Proof. by inj_tac; repeat (destruct val => //=; first by apply/eqP). Qed. Lemma R2_inj : injective R2. -Proof. by inj_tac; repeat (destruct val => //=; first by apply /eqP). Qed. +Proof. by inj_tac; repeat (destruct val => //=; first by apply/eqP). Qed. Lemma R3_inj : injective R3. -Proof. by inj_tac; repeat (destruct val => //=; first by apply /eqP). Qed. +Proof. by inj_tac; repeat (destruct val => //=; first by apply/eqP). Qed. Definition r1 := (perm R1_inj). Definition r2 := (perm R2_inj). @@ -97,8 +97,8 @@ Definition rot := [set r | is_rot r]. Lemma group_set_rot : group_set rot. Proof. -apply /group_setP;split; first by rewrite /rot inE /is_rot mulg1 mul1g. -move => x1 y; rewrite /rot !inE /= /is_rot; move/eqP => hx1; move/eqP => hy. +apply/group_setP; split; first by rewrite /rot inE /is_rot mulg1 mul1g. +move=> x1 y; rewrite /rot !inE /= /is_rot; move/eqP => hx1; move/eqP => hy. by rewrite -mulgA hy !mulgA hx1. Qed. @@ -111,15 +111,15 @@ Lemma rot_eq_c0 : forall r s : {perm square}, Proof. rewrite /is_rot => r s; move/eqP => hr; move/eqP=> hs hrs; apply/permP => a. have ->: a = (r1 ^+ a) c0 - by apply/eqP; case: a; do 4?case => //=; rewrite ?permM !permE. + by apply/eqP; case: a; do 4?case=> //=; rewrite ?permM !permE. by rewrite -!permM -!commuteX // !permM hrs. Qed. Lemma rot_r1 : forall r, is_rot r -> r = r1 ^+ (r c0). Proof. -move=> r hr;apply: rot_eq_c0 => //;apply/eqP. +move=> r hr; apply: rot_eq_c0 => //; apply/eqP. by symmetry; apply: commuteX. -by case: (r c0); do 4?case => //=; rewrite ?permM !permE /=. +by case: (r c0); do 4?case=> //=; rewrite ?permM !permE /=. Qed. Lemma rotations_is_rot : forall r, r \in rotations -> is_rot r. @@ -145,37 +145,37 @@ Definition Sh (sc : square) : square := tnth [tuple c1; c0; c3; c2] sc. Lemma Sh_inj : injective Sh. Proof. -by apply:(can_inj (g:= Sh)); case; do 4?case => //=;move=> H;apply /eqP. +by apply: (can_inj (g:= Sh)); case; do 4?case=> //=; move=> H; apply/eqP. Qed. Definition sh := (perm Sh_inj). Lemma sh_inv : sh^-1 = sh. Proof. -apply:(mulIg sh);rewrite mulVg ;apply/permP. -by case; do 4?case => //=; move=> H;rewrite !permE /= !permE; apply /eqP. +apply: (mulIg sh); rewrite mulVg; apply/permP. +by case; do 4?case=> //=; move=> H; rewrite !permE /= !permE; apply/eqP. Qed. Definition Sv (sc : square) : square := tnth [tuple c3; c2; c1; c0] sc. Lemma Sv_inj : injective Sv. Proof. -by apply : (can_inj (g:= Sv));case; do 4?case => //=;move => H;apply /eqP. +by apply: (can_inj (g:= Sv)); case; do 4?case=> //=; move=> H; apply/eqP. Qed. Definition sv := (perm Sv_inj). Lemma sv_inv : sv^-1 = sv. Proof. -apply:(mulIg sv);rewrite mulVg ;apply/permP. -by case; do 4?case => //=; move=> H; rewrite !permE /= !permE; apply /eqP. +apply: (mulIg sv); rewrite mulVg; apply/permP. +by case; do 4?case=> //=; move=> H; rewrite !permE /= !permE; apply/eqP. Qed. Definition Sd1 (sc : square) : square := tnth [tuple c0; c3; c2; c1] sc. Lemma Sd1_inj : injective Sd1. Proof. -by apply: can_inj Sd1 _; case; do 4?case=> //=; move=> H; apply /eqP. +by apply: can_inj Sd1 _; case; do 4?case=> //=; move=> H; apply/eqP. Qed. Definition sd1 := (perm Sd1_inj). @@ -183,14 +183,14 @@ Definition sd1 := (perm Sd1_inj). Lemma sd1_inv : sd1^-1 = sd1. Proof. apply: (mulIg sd1); rewrite mulVg; apply/permP. -by case; do 4?case=> //=; move=> H; rewrite !permE /= !permE; apply /eqP. +by case; do 4?case=> //=; move=> H; rewrite !permE /= !permE; apply/eqP. Qed. Definition Sd2 (sc : square) : square := tnth [tuple c2; c1; c0; c3] sc. Lemma Sd2_inj : injective Sd2. Proof. -by apply: can_inj Sd2 _; case; do 4?case=> //=; move=> H; apply /eqP. +by apply: can_inj Sd2 _; case; do 4?case=> //=; move=> H; apply/eqP. Qed. Definition sd2 := (perm Sd2_inj). @@ -238,8 +238,8 @@ Qed. Ltac non_inj p a1 a2 heq1 heq2 := let h1:= fresh "h1" in -(absurd (p a1 = p a2);first (by red; move=> h1;move:(perm_inj h1)); -by rewrite heq1 heq2;apply/eqP). +(absurd (p a1 = p a2); first (by red => - h1; move: (perm_inj h1)); +by rewrite heq1 heq2; apply/eqP). Ltac is_isoPtac p f e0 e1 e2 e3 := suff ->: p = f by [rewrite inE eqxx ?orbT]; @@ -444,7 +444,7 @@ move/eqn_pmul2l <-; rewrite -expnS -card_Fid Fid cardsT. rewrite -{1}[n]card_ord -cardX. pose pk k := [ffun i => k (if i == y then x else i) : colors]. rewrite -(@card_image _ _ (fun k : col_squares => (k y, pk k))). - apply/eqP; apply: eq_card => ck /=; rewrite inE /= [_ \in _]inE. + apply/eqP; apply: eq_card => ck /=; rewrite inE /= [_ \in _]inE. apply/eqP/imageP; last first. by case=> k _ -> /=; rewrite !ffunE if_same eqxx. case: ck => c k /= kxy. @@ -460,7 +460,7 @@ Qed. Lemma F_Sd2 : 'Fix_to[sd2] = [set x | coin0 x == coin2 x]. Proof. apply/setP => x; rewrite (sameP afix1P eqP) !inE eqperm_map /=. -by rewrite /act_f sd2_inv !ffunE !permE /= !eqxx !andbT eq_sym /= andbb. +by rewrite /act_f sd2_inv !ffunE !permE /= !eqxx !andbT eq_sym /= andbb. Qed. Lemma burnside_app_iso : @@ -555,19 +555,19 @@ Lemma S1_inv : involutive S1f. Proof. by move=> z; apply/eqP; case: z; do 6?case. Qed. Lemma S2_inv : involutive S2f. -Proof. by move=> z; apply /eqP; case: z; do 6?case. Qed. +Proof. by move=> z; apply/eqP; case: z; do 6?case. Qed. Lemma S3_inv : involutive S3f. -Proof. by move=> z; apply /eqP; case: z; do 6?case. Qed. +Proof. by move=> z; apply/eqP; case: z; do 6?case. Qed. Lemma S4_inv : involutive S4f. -Proof. by move=> z; apply /eqP; case: z; do 6?case. Qed. +Proof. by move=> z; apply/eqP; case: z; do 6?case. Qed. Lemma S5_inv : involutive S5f. -Proof. by move=> z; apply /eqP; case: z; do 6?case. Qed. +Proof. by move=> z; apply/eqP; case: z; do 6?case. Qed. Lemma S6_inv : involutive S6f. -Proof. by move=> z; apply /eqP; case: z; do 6?case. Qed. +Proof. by move=> z; apply/eqP; case: z; do 6?case. Qed. Lemma S05_inj : injective S05f. Proof. by apply: can_inj S05f _ => z; apply/eqP; case: z; do 6?case. Qed. @@ -594,10 +594,10 @@ Lemma R41_inj : injective R41f. Proof. by apply: can_inj R14f _ => z; apply/eqP; case: z; do 6?case. Qed. Lemma R32_inj : injective R32f. -Proof. by apply: can_inj R23f _ => z; apply /eqP; case: z; do 6?case. Qed. +Proof. by apply: can_inj R23f _ => z; apply/eqP; case: z; do 6?case. Qed. Lemma R024_inj : injective R024f. -Proof. by apply: can_inj R042f _ => z; apply /eqP; case: z ; do 6?case. Qed. +Proof. by apply: can_inj R042f _ => z; apply/eqP; case: z; do 6?case. Qed. Lemma R042_inj : injective R042f. Proof. by apply: can_inj R024f _ => z; apply/eqP; case: z; do 6?case. Qed. @@ -628,7 +628,7 @@ Definition s05 := (perm S05_inj). Definition s14 : {perm cube}. Proof. apply: (@perm _ S14f); apply: can_inj S14f _ => z. -by apply /eqP; case: z; do 6?case. +by apply/eqP; case: z; do 6?case. Defined. Definition s23 := (perm (inv_inj S23_inv)). @@ -661,8 +661,8 @@ Definition dir_iso3 := [set p | s1 == p, s2 == p, s3 == p, s4 == p, s5 == p | s6 == p]]. Definition dir_iso3l := [:: id3; s05; s14; s23; r05; r14; r23; r50; r41; - r32; r024; r042; r012; r021; r031; r013; r043 ; r034; - s1 ; s2; s3; s4; s5; s6]. + r32; r024; r042; r012; r021; r031; r013; r043; r034; + s1; s2; s3; s4; s5; s6]. Definition S0 := [:: F5; F4; F3; F2; F1; F0]. Definition S0f (sc : cube) : cube := tnth [tuple of S0] sc. @@ -730,8 +730,8 @@ by apply: eq_codom; apply: permE. Qed. Lemma Lcorrect : seq_iso_L == map sop [:: id3; s05; s14; s23; r05; r14; r23; - r50; r41; r32; r024; r042; r012; r021; r031; r013; r043 ; r034; - s1 ; s2; s3; s4; s5; s6]. + r50; r41; r32; r024; r042; r012; r021; r031; r013; r043; r034; + s1; s2; s3; s4; s5; s6]. Proof. by rewrite /= !seqs1. Qed. Lemma iso0_1 : dir_iso3 =i dir_iso3l. @@ -791,14 +791,14 @@ Qed. Ltac iso_tac := let a := fresh "a" in apply/permP => a; - apply/eqP; rewrite !permM !permE; case: a; do 6? case. + apply/eqP; rewrite !permM !permE; case: a; do 6?case. Ltac inv_tac := apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _; iso_tac. Lemma dir_s0p : forall p, (s0 * p) \in dir_iso3 -> p \notin dir_iso3. Proof. -move => p Hs0p; move: (ndir_s0p Hs0p); rewrite mulgA. +move=> p Hs0p; move: (ndir_s0p Hs0p); rewrite mulgA. have e: (s0^-1=s0) by inv_tac. by rewrite -{1}e mulVg mul1g. Qed. @@ -808,16 +808,16 @@ Definition iso3 := [set p | is_iso3b p]. Lemma is_iso3P : forall p, reflect (is_iso3 p) (p \in iso3). Proof. -move => p; apply: (iffP idP); rewrite inE /iso3 /is_iso3b /is_iso3 => e. - by move => fi; rewrite -!permM (eqP e). -by apply/eqP;apply/permP=> z; rewrite !permM (e z). +move=> p; apply: (iffP idP); rewrite inE /iso3 /is_iso3b /is_iso3 => e. + by move=> fi; rewrite -!permM (eqP e). +by apply/eqP; apply/permP=> z; rewrite !permM (e z). Qed. Lemma group_set_iso3 : group_set iso3. Proof. -apply /group_setP;split. +apply/group_setP; split. by apply/is_iso3P => fi; rewrite -!permM mulg1 mul1g. -move => x1 y; rewrite /iso3 !inE /= /is_iso3. +move=> x1 y; rewrite /iso3 !inE /= /is_iso3. rewrite /is_iso3b. rewrite -mulgA. move/eqP => hx1; move/eqP => hy. @@ -828,16 +828,16 @@ Canonical iso_group3 := Group group_set_iso3. Lemma group_set_diso3 : group_set dir_iso3. Proof. -apply/group_setP;split;first by rewrite inE eqxx /=. -by apply:stable. +apply/group_setP; split; first by rewrite inE eqxx /=. +by apply: stable. Qed. Canonical diso_group3 := Group group_set_diso3. Lemma gen_diso3 : dir_iso3 = <<[set r05; r14]>>. Proof. -apply/setP; apply/subset_eqP;apply/andP; split;first last. - by rewrite gen_subG;apply/subsetP => x; rewrite !inE; - case/orP; move/eqP ->; rewrite eqxx !orbT. +apply/setP; apply/subset_eqP; apply/andP; split; first last. + by rewrite gen_subG; apply/subsetP => x; rewrite !inE; + case/orP; move/eqP ->; rewrite eqxx !orbT. apply/subsetP => x; rewrite !inE. have -> : s05 = r05 * r05 by iso_tac. have -> : s14 = r14 * r14 by iso_tac. @@ -910,7 +910,7 @@ Proof. have s05_inv: s05^-1=s05 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s05_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= andbT/col1/col2/col3/col4/col5/col0. -by do 2![rewrite eq_sym; case : {+}(_ == _)=> //= ]. +by do 2![rewrite eq_sym; case: {+}(_ == _)=> //= ]. Qed. Lemma F_s14 : @@ -919,7 +919,7 @@ Proof. have s14_inv: s14^-1=s14 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s14_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= andbT/col1/col2/col3/col4/col5/col0. -by do 2![rewrite eq_sym; case : {+}(_ == _)=> //= ]. +by do 2![rewrite eq_sym; case: {+}(_ == _)=> //= ]. Qed. Lemma r05_inv : r05^-1 = r50. @@ -942,7 +942,7 @@ Lemma F_s23 : Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s23_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= andbT/col1/col2/col3/col4/col5/col0. -by do 2![rewrite eq_sym; case : {+}(_ == _)=> //=]. +by do 2![rewrite eq_sym; case: {+}(_ == _)=> //=]. Qed. Lemma F_r05 : 'Fix_to_g[r05]= @@ -952,7 +952,7 @@ Proof. apply sym_equal. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r05_inv !ffunE !permE /=. rewrite !eqxx /= !andbT /col1/col2/col3/col4/col5/col0. -by do 3! [rewrite eq_sym;case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ]. +by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ]. Qed. Lemma F_r50 : 'Fix_to_g[r50]= @@ -960,8 +960,8 @@ Lemma F_r50 : 'Fix_to_g[r50]= && (col3 x == col4 x)]. Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r50_inv !ffunE !permE /=. -apply sym_equal;rewrite !eqxx /= !andbT /col1/col2/col3/col4. -by do 3![rewrite eq_sym;case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ]. +apply sym_equal; rewrite !eqxx /= !andbT /col1/col2/col3/col4. +by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ]. Qed. Lemma F_r23 : 'Fix_to_g[r23] = @@ -1137,10 +1137,10 @@ Qed. Lemma uniq4_uniq6 : forall x y z t : cube, uniq [:: x; y; z; t] -> exists u, exists v, uniq [:: x; y; z; t; u; v]. Proof. -move => x y z t Uxt; move:( cardC (mem [:: x; y; z; t])). +move=> x y z t Uxt; move: ( cardC (mem [:: x; y; z; t])). rewrite card_ord (card_uniq_tuple Uxt) => hcard. have hcard2: #|predC (mem [:: x; y; z; t])| = 2. - by apply:( @addnI 4); rewrite /injective hcard. + by apply: ( @addnI 4); rewrite /injective hcard. have: #|predC (mem [:: x; y; z; t])| != 0 by rewrite hcard2. case/existsP=> u Hu; exists u. move: (cardC (mem [:: x; y; z; t; u])); rewrite card_ord => hcard5. @@ -1150,62 +1150,62 @@ have: #|[predC [:: x; y; z; t; u]]| !=0. case/existsP=> v; rewrite inE (mem_cat _ [:: _; _; _; _]). case/norP=> Hv Huv; exists v. rewrite (cat_uniq [:: x; y; z; t]) Uxt andTb. -by rewrite -rev_uniq /= negb_or Hu orbF Hv Huv. +by rewrite -rev_uniq /= negb_or Hu orbF Hv Huv. Qed. Lemma card_n4 : forall x y z t : cube, uniq [:: x; y; z; t] -> #|[set p : col_cubes | (p x == p y) && (p z == p t)]| = (n ^ 4)%N. Proof. move=> x y z t Uxt. rewrite -[n]card_ord . -case:(uniq4_uniq6 Uxt) => u; case => v Uxv. +case: (uniq4_uniq6 Uxt) => u; case=> v Uxv. pose ff (p : col_cubes) := (p x, p z, p u , p v). rewrite -(@card_in_image _ _ ff); first last. move=> p1 p2; rewrite !inE. case/andP=> p1y p1t; case/andP=> p2y p2t [px pz] pu pv. - have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u ; v]. + have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u; v]. by rewrite /= -(eqP p1y) -(eqP p1t) -(eqP p2y) -(eqP p2t) px pz pu pv !eqxx. apply/ffunP=> i; apply/eqP; apply: (allP eqp12). by rewrite (subset_cardP _ (subset_predT _)) // (card_uniqP Uxv) card_ord. have ->:forall n, (n ^ 4)%N= (n*n*n*n)%N. - by move => n0;rewrite (expnD n0 2 2) -mulnn mulnA. + by move=> n0; rewrite (expnD n0 2 2) -mulnn mulnA. rewrite -!card_prod; apply: eq_card => [] [[[c d]e ]g] /=; apply/imageP. -rewrite (cat_uniq [::x; y;z;t]) in Uxv; case/and3P: Uxv => _ hasxt. +rewrite (cat_uniq [::x; y; z; t]) in Uxv; case/and3P: Uxv => _ hasxt. rewrite /= !inE andbT. move/negbTE=> nuv . rewrite (cat_uniq [::x; y]) in Uxt; case/and3P: Uxt => _. rewrite /= !andbT orbF; case/norP; rewrite !inE => nxyz nxyt _. -move:hasxt; rewrite /= !orbF; case/norP; rewrite !inE orbA. +move: hasxt; rewrite /= !orbF; case/norP; rewrite !inE orbA. case/norP => nxyu nztu. -rewrite orbA;case/norP=> nxyv nztv. +rewrite orbA; case/norP=> nxyv nztv. exists [ffun i => if pred2 x y i then c else if pred2 z t i then d else if u==i then e else g]. rewrite !inE /= !ffunE //= !eqxx orbT //= !eqxx /= orbT. by rewrite (negbTE nxyz) (negbTE nxyt). rewrite {}/ff !ffunE /= !eqxx /=. rewrite (negbTE nxyz) (negbTE nxyu) (negbTE nztu) (negbTE nxyv) (negbTE nztv). -by rewrite nuv. +by rewrite nuv. Qed. -Lemma card_n3_3 : forall x y z t: cube, uniq [:: x; y; z;t] -> +Lemma card_n3_3 : forall x y z t: cube, uniq [:: x; y; z; t] -> #|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p z == p t)]| = (n ^ 3)%N. Proof. move=> x y z t Uxt; rewrite -[n]card_ord . -case:(uniq4_uniq6 Uxt) => u; case => v Uxv. +case: (uniq4_uniq6 Uxt) => u; case=> v Uxv. pose ff (p : col_cubes) := (p x, p u , p v); rewrite -(@card_in_image _ _ ff); first last. move=> p1 p2; rewrite !inE. - case/andP ;case/andP => p1xy p1yz p1zt. - case/andP ;case/andP => p2xy p2yz p2zt [px pu] pv. - have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u ; v]. + case/andP; case/andP => p1xy p1yz p1zt. + case/andP; case/andP => p2xy p2yz p2zt [px pu] pv. + have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u; v]. by rewrite /= -(eqP p1zt) -(eqP p2zt) -(eqP p1yz) -(eqP p2yz) -(eqP p1xy) -(eqP p2xy) px pu pv !eqxx. apply/ffunP=> i; apply/eqP; apply: (allP eqp12). by rewrite (subset_cardP _ (subset_predT _)) // (card_uniqP Uxv) card_ord. have ->:forall n, (n ^ 3)%N= (n*n*n)%N. - by move => n0 ; rewrite (expnD n0 2 1) -mulnn expn1. + by move=> n0; rewrite (expnD n0 2 1) -mulnn expn1. rewrite -!card_prod; apply: eq_card => [] [[c d]e ] /=; apply/imageP. -rewrite (cat_uniq [::x; y;z;t]) in Uxv; case/and3P: Uxv => _ hasxt. +rewrite (cat_uniq [::x; y; z; t]) in Uxv; case/and3P: Uxv => _ hasxt. rewrite /uniq !inE !andbT; move/negbTE=> nuv. exists [ffun i => if (i \in [:: x; y; z; t]) then c else if u == i then d else e]. @@ -1214,24 +1214,24 @@ rewrite {}/ff !ffunE !inE /= !eqxx /=; move: hasxt; rewrite nuv. by do 8![case E: ( _ == _ ); rewrite ?(eqP E)/= ?inE ?eqxx //= ?E {E}]. Qed. -Lemma card_n2_3 : forall x y z t u v: cube, uniq [:: x; y; z;t; u ; v] -> +Lemma card_n2_3 : forall x y z t u v: cube, uniq [:: x; y; z; t; u; v] -> #|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p t == p u ) && (p u== p v)]| = (n ^ 2)%N. Proof. move=> x y z t u v Uxv; rewrite -[n]card_ord . pose ff (p : col_cubes) := (p x, p t); rewrite -(@card_in_image _ _ ff); first last. move=> p1 p2; rewrite !inE. - case/andP ;case/andP ; case/andP => p1xy p1yz p1tu p1uv. - case/andP ;case/andP; case/andP => p2xy p2yz p2tu p2uv [px pu]. - have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u ; v]. + case/andP; case/andP; case/andP => p1xy p1yz p1tu p1uv. + case/andP; case/andP; case/andP => p2xy p2yz p2tu p2uv [px pu]. + have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u; v]. by rewrite /= -(eqP p1yz) -(eqP p2yz) -(eqP p1xy) -(eqP p2xy) -(eqP p1uv) -(eqP p2uv) -(eqP p1tu) -(eqP p2tu) px pu !eqxx. apply/ffunP=> i; apply/eqP; apply: (allP eqp12). by rewrite (subset_cardP _ (subset_predT _)) // (card_uniqP Uxv) card_ord. -have ->:forall n, (n ^ 2)%N= (n*n)%N by move => n0 ; rewrite -mulnn . +have ->:forall n, (n ^ 2)%N= (n*n)%N by move=> n0; rewrite -mulnn . rewrite -!card_prod; apply: eq_card => [] [c d]/=; apply/imageP. -rewrite (cat_uniq [::x; y;z]) in Uxv; case/and3P: Uxv => Uxt hasxt nuv . -move:hasxt;rewrite /= !orbF; case/norP; rewrite !inE => nxyzt. +rewrite (cat_uniq [::x; y; z]) in Uxv; case/and3P: Uxv => Uxt hasxt nuv . +move: hasxt; rewrite /= !orbF; case/norP; rewrite !inE => nxyzt. case/norP => nxyzu nxyzv. exists [ffun i => if (i \in [:: x; y; z] ) then c else d]. rewrite !inE /= !ffunE !inE //= !eqxx !orbT !eqxx //=. @@ -1239,7 +1239,7 @@ exists [ffun i => if (i \in [:: x; y; z] ) then c else d]. by rewrite {}/ff !ffunE !inE /= !eqxx /= (negbTE nxyzt). Qed. -Lemma card_n3s : forall x y z t u v: cube, uniq [:: x; y; z;t; u ; v] -> +Lemma card_n3s : forall x y z t u v: cube, uniq [:: x; y; z; t; u; v] -> #|[set p : col_cubes | (p x == p y) && (p z == p t)&& (p u == p v )]| = (n ^ 3)%N. Proof. @@ -1247,22 +1247,22 @@ move=> x y z t u v Uxv; rewrite -[n]card_ord . pose ff (p : col_cubes) := (p x, p z, p u). rewrite -(@card_in_image _ _ ff); first last. move=> p1 p2; rewrite !inE. - case/andP ;case/andP => p1xy p1zt p1uv. - case/andP ;case/andP => p2xy p2zt p2uv [px pz] pu. - have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u ; v]. + case/andP; case/andP => p1xy p1zt p1uv. + case/andP; case/andP => p2xy p2zt p2uv [px pz] pu. + have eqp12: all (fun i => p1 i == p2 i) [:: x; y; z; t; u; v]. by rewrite /= -(eqP p1xy) -(eqP p2xy) -(eqP p1zt) -(eqP p2zt) -(eqP p1uv) -(eqP p2uv) px pz pu !eqxx. apply/ffunP=> i; apply/eqP; apply: (allP eqp12). by rewrite (subset_cardP _ (subset_predT _)) // (card_uniqP Uxv) card_ord. have ->:forall n, (n ^ 3)%N= (n*n*n)%N. - by move => n0 ; rewrite (expnD n0 2 1) -mulnn expn1. + by move=> n0; rewrite (expnD n0 2 1) -mulnn expn1. rewrite -!card_prod. apply: eq_card => [] [[c d]e ] /=; apply/imageP. -rewrite (cat_uniq [::x; y;z;t]) in Uxv; case/and3P: Uxv => Uxt hasxt nuv . +rewrite (cat_uniq [::x; y; z; t]) in Uxv; case/and3P: Uxv => Uxt hasxt nuv . rewrite (cat_uniq [::x; y]) in Uxt; case/and3P: Uxt => _. -rewrite /= !orbF !andbT; case/norP ; rewrite !inE => nxyz nxyt _. +rewrite /= !orbF !andbT; case/norP; rewrite !inE => nxyz nxyt _. move: hasxt; rewrite /= !orbF; case/norP; rewrite !inE orbA. case/norP => nxyu nztu. -rewrite orbA;case/norP=> nxyv nztv. +rewrite orbA; case/norP=> nxyv nztv. exists [ffun i => if (i \in [:: x; y] ) then c else if (i \in [:: z; t] ) then d else e]. rewrite !inE /= !ffunE !inE // !eqxx !orbT !eqxx //=. @@ -1276,15 +1276,15 @@ Lemma burnside_app_iso3 : (cube_coloring_number24 * 24 = n ^ 6 + 6 * n ^ 3 + 3 * n ^ 4 + 8 * (n ^ 2) + 6 * n ^ 3)%N. Proof. -pose iso_list :=[::id3; s05; s14; s23; r05; r14; r23; r50; r41; r32; - r024; r042; r012; r021; r031; r013; r043 ; r034; - s1 ; s2; s3; s4; s5; s6]. +pose iso_list :=[::id3; s05; s14; s23; r05; r14; r23; r50; r41; r32; + r024; r042; r012; r021; r031; r013; r043; r034; + s1; s2; s3; s4; s5; s6]. rewrite (burnside_formula iso_list) => [||p]; last first. -- by rewrite !inE /= !(eq_sym _ p). +- by rewrite !inE /= !(eq_sym _ p). - apply: map_uniq (fun p : {perm cube} => (p F0, p F1)) _ _. have bsr:(fun p : {perm cube} => (p F0, p F1)) =1 (fun p => (nth F0 p F0, nth F0 p F1)) \o sop. - by move => x; rewrite /= -2!sop_spec. + by move=> x; rewrite /= -2!sop_spec. by rewrite (eq_map bsr) map_comp -(eqP Lcorrect); vm_compute. rewrite !big_cons big_nil {1}card_Fid3 /= F_s05 F_s14 F_s23 F_r05 F_r14 F_r23 F_r50 F_r41 F_r32 F_r024 F_r042 F_r012 F_r021 F_r031 F_r013 F_r043 F_r034 diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index d63c302..54726be 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -70,7 +70,7 @@ Canonical center_pgFun := [pgFun by morphim_center]. Section Center. Variables gT : finGroupType. -Implicit Type rT : finGroupType. +Implicit Type rT : finGroupType. Implicit Types (x y : gT) (A B : {set gT}) (G H K D : {group gT}). Lemma subcentP A B x : reflect (x \in A /\ centralises x B) (x \in 'C_A(B)). @@ -101,7 +101,7 @@ Proof. exact: subcentP. Qed. Lemma center_sub A : 'Z(A) \subset A. Proof. exact: subsetIl. Qed. -Lemma center1 : 'Z(1) = 1 :> {set gT}. +Lemma center1 : 'Z(1) = 1 :> {set gT}. Proof. exact: gF1. Qed. Lemma centerC A : {in A, centralised 'Z(A)}. @@ -338,7 +338,7 @@ Proof. transitivity ('ker (subg [group of setX H K / kerHK] \o coset kerHK)). rewrite /ker /morphpre /= /in_cprod /cprod_by; case: cprod_by_key => /=. by rewrite ['N(_) :&: _]quotientGK ?sub_center_normal ?ker_cprod_by_central. -by rewrite ker_comp ker_subg -kerE ker_coset. +by rewrite ker_comp ker_subg -kerE ker_coset. Qed. Lemma cpairg1_dom : H \subset 'dom (in_cprod \o @pairg1 gTH gTK). diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index f3e0779..1f9bad0 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -272,7 +272,7 @@ Qed. Lemma der1_joing_cycles (x y : gT) : let XY := <[x]> <*> <[y]> in let xy := [~ x, y] in xy \in 'C(XY) -> XY^`(1) = <[xy]>. -Proof. +Proof. rewrite joing_idl joing_idr /= -sub_cent1 => /norms_gen nRxy. apply/eqP; rewrite eqEsubset cycle_subG mem_commg ?mem_gen ?set21 ?set22 //. rewrite der1_min // quotient_gen -1?gen_subG // quotientU abelian_gen. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index 8073449..9a1e451 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -316,7 +316,7 @@ Hypothesis dvd_y_x : #[y] %| #[x]. Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i. Proof. apply/eqP; rewrite eq_expg_mod_order. -have [x_le1 | x_gt1] := leqP #[x] 1. +have [x_le1 | x_gt1] := leqP #[x] 1. suffices: #[y] %| 1 by rewrite dvdn1 => /eqP->; rewrite !modn1. by rewrite (dvdn_trans dvd_y_x) // dvdn1 order_eq1 -cycle_eq1 trivg_card_le1. rewrite -(expg_znat i (cycle_id x)) invmE /=; last by rewrite /Zp x_gt1 inE. @@ -536,7 +536,7 @@ Lemma metacyclicP A : Proof. exact: 'exists_and3P. Qed. Lemma metacyclic1 : metacyclic 1. -Proof. +Proof. by apply/existsP; exists 1%G; rewrite normal1 trivg_quotient !cyclic1. Qed. diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 9d158cc..2c7f6c3 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -127,7 +127,7 @@ Qed. Lemma Grp_pX1p2 : p^{1+2} \isog Grp (x : y : (x ^+ p, y ^+ p, [~ x, y, x], [~ x, y, y])). Proof. -rewrite [@gtype _]unlock ; apply: intro_isoGrp => [|rT H]. +rewrite [@gtype _]unlock; apply: intro_isoGrp => [|rT H]. apply/existsP; pose x := sdpair1 actp (0, 1)%R; pose y := sdpair2 actp 1%R. exists (x, y); rewrite /= !xpair_eqE; set z := [~ x, y]; set G := _ <*> _. have def_z: z = sdpair1 actp (1, 0)%R. @@ -463,7 +463,7 @@ have ox: #[x] = p. have defCy: 'C_G(Y) = Z * <[x]>. apply/eqP; rewrite eq_sym eqEcard mulG_subG setIS ?centS //=. rewrite cycle_subG inE Gx cYx oCY TI_cardMg ?oZ -?orderE ?ox //=. - by rewrite setIC prime_TIg -?orderE ?ox ?cycle_subG. + by rewrite setIC prime_TIg -?orderE ?ox ?cycle_subG. have abelYt: p.-abelem (Y / Z). by rewrite (abelemS (quotientS _ sYG)) //= -/Z -defPhiG Phi_quotient_abelem. have Yxt: coset Z x \in Y / Z by rewrite mem_quotient. diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 342eeae..9ac5236 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -343,7 +343,7 @@ have [ms0 os0]: m s0 = (p ^ n).+1%:R /\ #[s0] = p. rewrite subnK // mulSn -mulnA -expnS -addSn natrD natrM -oG char_Zp //. rewrite mulr0 addr0 => m_s0; split => //. have [d _] := m_se (n - e0)%N; rewrite -subnSK // expnSr expgM -/s0. - rewrite addSn subnK // -oG mulrS natrM char_Zp // {d}mulr0 addr0. + rewrite addSn subnK // -oG mulrS natrM char_Zp // {d}mulr0 addr0. move/eqP; rewrite -m1 (inj_in_eq inj_m) ?group1 ?groupX // -order_dvdn. move/min_p; rewrite order_eq1; case/predU1P=> [s0_1 | ]; last by move/eqP. move/eqP: m_s0; rewrite eq_sym s0_1 m1 -subr_eq0 mulrSr addrK -val_eqE /=. @@ -361,7 +361,7 @@ have defS1: 'Ohm_1(<[s]>) = <[s0]>. rewrite (Ohm1_cyclic_pgroup_prime _ p_s) ?cycle_cyclic ?leqnn ?cycle_eq1 //=. rewrite (OhmE _ p_s) mem_gen ?groupX //= !inE mem_cycle //. by rewrite -order_dvdn os0 ?dvdnn. - by apply/eqP=> s1; rewrite -os0 /s0 s1 expg1n order1 in p_gt1. + by apply/eqP=> s1; rewrite -os0 /s0 s1 expg1n order1 in p_gt1. case: (even_prime p_pr) => [p2 | oddp]; last first. rewrite {+}/e0 oddp subn0 in s0 os0 ms0 os ms defS1 *. have [f defF] := cyclicP cycF; have defP: P = <[s]>. @@ -591,7 +591,7 @@ rewrite (mulnC r) /r {1}def_n expnSr mulnA -mulnDl -mulnA -expnS. rewrite subnSK // subn2 /q -def_n1 expnS dvdn_pmul2r // dvdn_addl. by case/dvdnP=> k ->; rewrite mulnC expgM mem_mulg ?mem_cycle. case: (ltngtP n 3) => [|n_gt3|n3]; first by rewrite ltnNge n_gt2. - by rewrite -subnSK // expnSr mulnA dvdn_mull. + by rewrite -subnSK // expnSr mulnA dvdn_mull. case: (even_prime p_pr) notG8 => [-> | oddp _]; first by rewrite n3. by rewrite bin2odd // -!mulnA dvdn_mulr. Qed. @@ -756,7 +756,7 @@ set B := [set: gT] => oB; set K := _ :\: _. case/existsP=> -[u v] /= /eqP[defB uq v4 uv]. have nUV: <[v]> \subset 'N(<[u]>) by rewrite norms_cycle uv groupV cycle_id. rewrite norm_joinEr // in defB. -have le_ou: #[u] <= q by rewrite dvdn_leq ?expn_gt0 // order_dvdn uq. +have le_ou: #[u] <= q by rewrite dvdn_leq ?expn_gt0 // order_dvdn uq. have le_ov: #[v] <= 4 by rewrite dvdn_leq // order_dvdn v4. have tiUV: <[u]> :&: <[v]> = 1 by rewrite cardMg_TI // defB oB leq_mul. have{le_ou le_ov} [ou ov]: #[u] = q /\ #[v] = 4. @@ -1011,7 +1011,7 @@ have def_tG: {in G :\: X, forall t, t ^: G = <[x ^+ 2]> :* t}. move=> t X't; have [Gt notXt] := setDP X't. have defJt: {in X, forall z, t ^ z = z ^- 2 * t}. move=> z Xz; rewrite /= invMg -mulgA (conjgC _ t). - by rewrite (invXX' _ t) ?groupV ?invgK. + by rewrite (invXX' _ t) ?groupV ?invgK. have defGt: X * <[t]> = G by rewrite (mulg_normal_maximal nsXG) ?cycle_subG. apply/setP=> tz; apply/imsetP/rcosetP=> [[t'z] | [z]]. rewrite -defGt -normC ?cycle_subG ?(subsetP nXG) //. @@ -1067,7 +1067,7 @@ split. - split=> //= H; apply/idP/idP=> [maxH |]; last first. by case/or3P=> /eqP->; rewrite ?maxMt. have [sHG nHG]:= andP (p_maximal_normal pG maxH). - have oH: #|H| = q. + have oH: #|H| = q. apply: double_inj; rewrite -muln2 -(p_maximal_index pG maxH) Lagrange //. by rewrite oG -mul2n. rewrite !(eq_sym (gval H)) -eq_sym !eqEcard oH -orderE ox !oMt // !leqnn. @@ -1212,7 +1212,7 @@ have def_tG: {in G :\: X, forall t, t ^: G = <[x ^+ 2]> :* t}. move=> t X't; have [Gt notXt] := setDP X't. have defJt: {in X, forall z, t ^ z = z ^- 2 * t}. move=> z Xz; rewrite /= invMg -mulgA (conjgC _ t). - by rewrite (invXX' _ t) ?groupV ?invgK. + by rewrite (invXX' _ t) ?groupV ?invgK. have defGt: X * <[t]> = G by rewrite (mulg_normal_maximal nsXG) ?cycle_subG. apply/setP=> tz; apply/imsetP/rcosetP=> [[t'z] | [z]]. rewrite -defGt -normC ?cycle_subG ?(subsetP nXG) //. @@ -1795,7 +1795,7 @@ have p_i: p %| i. case=> [[n_gt23 xy] | [p2 Z_xxy]]. suffices ->: cG = ModularGroup by []; apply/modular_group_classP. exists p => //; exists n => //; rewrite isogEcard card_modular_group //. - rewrite oG leqnn andbT Grp_modular_group // -/q -/r. + rewrite oG leqnn andbT Grp_modular_group // -/q -/r. have{i def_yp p_i} [i def_yp]: exists i, y ^- p = x ^+ i ^+ p. by case/dvdnP: p_i => j def_i; exists j; rewrite -expgM -def_i. have Zyx: [~ y, x] \in Z. @@ -1825,7 +1825,7 @@ case=> [[n_gt23 xy] | [p2 Z_xxy]]. by rewrite -p2 -oZ order_dvdG. have{i def_yp p_i} Zy2: y ^+ 2 \in Z. rewrite defZ (OhmE _ pX) -groupV -p2 def_yp mem_gen // !inE groupX //= p2. - rewrite expgS -{2}def_yp -(mulKg y y) -conjgE -conjXg -conjVg def_yp conjXg. + rewrite expgS -{2}def_yp -(mulKg y y) -conjgE -conjXg -conjVg def_yp conjXg. rewrite -expgMn //; last by apply: (centsP cXX); rewrite ?memJ_norm. by rewrite -order_dvdn (dvdn_trans (order_dvdG Z_xxy)) ?oZ. rewrite !cycle_traject !orderE oZ p2 !inE !mulg1 /= in Z_xxy Zy2 *. diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v index 97b2ebc..5a2b35b 100644 --- a/mathcomp/solvable/finmodule.v +++ b/mathcomp/solvable/finmodule.v @@ -140,13 +140,13 @@ Canonical fmod_morphism := Morphism fmodM. Lemma fmodX n : {in A, {morph fmod : x / (x ^+ n)%g >-> x *+ n}}. Proof. exact: morphX. Qed. Lemma fmodV : {morph fmod : x / x^-1%g >-> - x}. -Proof. +Proof. move=> x; apply: val_inj; rewrite fmvalN !fmodKcond groupV. by case: (x \in A); rewrite ?invg1. Qed. Lemma injm_fmod : 'injm fmod. -Proof. +Proof. by apply/injmP=> x y Ax Ay []; move/val_inj; apply: (injmP (injm_subg A)). Qed. @@ -212,13 +212,13 @@ Proof. by move=> x y Nx Ny /= u; apply: val_inj; rewrite !fmvalJ ?conjgM ?groupM. Qed. -Lemma actrK x : cancel (actr^~ x) (actr^~ x^-1%g). +Lemma actrK x : cancel (actr^~ x) (actr^~ x^-1%g). Proof. move=> u; apply: val_inj; rewrite !fmvalJcond groupV. by case: ifP => -> //; rewrite conjgK. Qed. -Lemma actrKV x : cancel (actr^~ x^-1%g) (actr^~ x). +Lemma actrKV x : cancel (actr^~ x^-1%g) (actr^~ x). Proof. by move=> u; rewrite /= -{2}(invgK x) actrK. Qed. End OneFinMod. @@ -330,7 +330,7 @@ have{cocycle_nu} fM: {in G &, {morph f : x y / x * y}}. move=> x y Gx Gy; rewrite /f ?rHmul // -3!mulgA; congr (_ * _). rewrite (mulgA _ (rH y)) (conjgC _ (rH y)) -mulgA; congr (_ * _). rewrite -fmvalJ ?actrH ?nHG ?GrH // -!fmvalA actZr -mulrnDl. - rewrite -(addrC (nu y)) cocycle_nu // mulrnDl !fmvalA; congr (_ * _). + rewrite -(addrC (nu y)) cocycle_nu // mulrnDl !fmvalA; congr (_ * _). by rewrite !fmvalZ expgK ?fmodP. exists (Morphism fM @* G)%G; apply/complP; split. apply/trivgP/subsetP=> x /setIP[Hx /morphimP[y _ Gy eq_x]]. @@ -479,7 +479,7 @@ Lemma mulg_exp_card_rcosets x : x * (g ^+ n_ x) \in H :* x. Proof. rewrite /n_ /indexg -orbitRs -pcycle_actperm ?inE //. rewrite -{2}(iter_pcycle (actperm 'Rs g) (H :* x)) -permX -morphX ?inE //. -by rewrite actpermE //= rcosetE -rcosetM rcoset_refl. +by rewrite actpermE //= rcosetE -rcosetM rcoset_refl. Qed. Let HGg : {set {set {set gT}}} := orbit 'Rs <[g]> @: HG. @@ -545,9 +545,9 @@ have pcyc_eq x: pcyc x =i traj x by apply: pcycle_traject. have uniq_traj x: uniq (traj x) by apply: uniq_traject_pcycle. have n_eq x: n_ x = #|pcyc x| by rewrite -Hgr_eq. have size_traj x: size (traj x) = n_ x by rewrite n_eq size_traject. -have nth_traj x j: j < n_ x -> nth (H :* x) (traj x) j = H :* (x * g ^+ j). +have nth_traj x j: j < n_ x -> nth (H :* x) (traj x) j = H :* (x * g ^+ j). move=> lt_j_x; rewrite nth_traject -?n_eq //. - by rewrite -permX -morphX ?inE // actpermE //= rcosetE rcosetM. + by rewrite -permX -morphX ?inE // actpermE //= rcosetE rcosetM. have sYG: Y \subset G. apply/bigcupsP=> x Xx; apply/subsetP=> _ /imsetP[i _ ->]. by rewrite groupM ?groupX // sXG. @@ -586,7 +586,7 @@ rewrite /traj -n_eq; case def_n: (n_ x) (n_gt0) => // [n] _. rewrite conjgE invgK -{1}[H :* x]rcoset1 -{1}(expg0 g). elim: {1 3}n 0%N (addn0 n) => [|m IHm] i def_i /=. rewrite big_seq1 {i}[i]def_i rYE // ?def_n //. - rewrite -(mulgA _ _ g) -rcosetM -expgSr -[(H :* x) :* _]rcosetE. + rewrite -(mulgA _ _ g) -rcosetM -expgSr -[(H :* x) :* _]rcosetE. rewrite -actpermE morphX ?inE // permX // -{2}def_n n_eq iter_pcycle mulgA. by rewrite -[H :* x]rcoset1 (rYE _ 0%N) ?mulg1. rewrite big_cons rYE //; last by rewrite def_n -def_i ltnS leq_addl. diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index e4a716d..da65950 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -567,7 +567,7 @@ have hallK: Hall G K. rewrite !inE -andbA -sub_cent1=> /and4P[_ Kz _ cPz] ntz. by apply: subset_trans (regK z _); [apply/subsetIP | apply/setD1P]. have /splitsP[H /complP[tiKH defG]] := SchurZassenhaus_split hallK nsKG. -have [_ sHG] := mulG_sub defG; have nKH := subset_trans sHG nKG. +have [_ sHG] := mulG_sub defG; have nKH := subset_trans sHG nKG. exists H; apply/Frobenius_semiregularP; rewrite ?sdprodE //. by apply: contraNneq (proper_subn ltKG) => H1; rewrite -defG H1 mulg1. apply: semiregular_sym => x Kx; apply/trivgP; rewrite -tiKH. @@ -603,7 +603,7 @@ have partG: partition (gval K |: (H^# :^: K)) G. apply: Frobenius_partition; apply/andP; rewrite defG; split=> //. by apply/Frobenius_actionP; apply: HasFrobeniusAction FrobG. have{FrobG} [ffulG transG regG ntH [u Su defH]]:= FrobG. -apply/setP=> x; rewrite !inE; have [-> | ntx] := altP eqP; first exact: group1. +apply/setP=> x; rewrite !inE; have [-> | ntx] := altP eqP; first exact: group1. rewrite /= -(cover_partition partG) /cover. have neKHy y: gval K <> H^# :^ y. by move/setP/(_ 1); rewrite group1 conjD1g setD11. diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index fc8385d..7fbee8c 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -158,7 +158,7 @@ End Definitions. Section ClassDefinitions. Structure iso_map := IsoMap { - apply : object_map; + apply: object_map; _ : group_valued apply; _ : closed apply; _ : iso_continuous apply diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 772db33..6dcd833 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -420,7 +420,7 @@ Qed. Lemma maxnormal_minnormal G L M : G \subset 'N(M) -> L \subset 'N(G) -> maxnormal M G L -> - minnormal (G / M) (L / M). + minnormal (G / M) (L / M). Proof. move=> nMG nGL /maxgroupP[/andP[/andP[sMG ltMG] nML] maxM]; apply/mingroupP. rewrite -subG1 quotient_sub1 ?ltMG ?quotient_norms //. @@ -544,7 +544,7 @@ Proof. by case/and3P=> /quotient_cents2r *; rewrite subsetI quotientS. Qed. Lemma central_central_factor H K : (K / H) \subset 'Z(G / H) -> H <| K -> H <| G -> central_factor G H K. Proof. -case/subsetIP=> sKGb cGKb /andP[sHK nHK] /andP[sHG nHG]. +case/subsetIP=> sKGb cGKb /andP[sHK nHK] /andP[sHG nHG]. by rewrite /central_factor -quotient_cents2 // cGKb sHK -(quotientSGK nHK). Qed. diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index d59964b..68c2863 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.v @@ -291,7 +291,7 @@ case: (SchurZassenhaus_trans_sol _ nMK sK1G1 coMK) => [||x Mx defK1]. by apply/trivgP; rewrite -trMH /= setIA subsetIl. rewrite -coprime_cardMg // defG1; apply/eqP; congr #|(_ : {set _})|. rewrite group_modl; last by rewrite -defG1 mulG_subl. - by apply/setIidPr; rewrite defG gen_subG subUset sKG. + by apply/setIidPr; rewrite defG gen_subG subUset sKG. exists x^-1; first by rewrite groupV (subsetP sMG). by rewrite -(_ : K1 :^ x^-1 = K) ?(conjSg, subsetIl) // defK1 conjsgK. Qed. @@ -310,7 +310,7 @@ Corollary Hall_trans pi (G H1 H2 : {group gT}) : solvable G -> pi.-Hall(G) H1 -> pi.-Hall(G) H2 -> exists2 x, x \in G & H1 :=: H2 :^ x. Proof. -move=> solG; have [H hallH transH] := Hall_exists_subJ pi solG. +move=> solG; have [H hallH transH] := Hall_exists_subJ pi solG. have conjH (K : {group gT}): pi.-Hall(G) K -> exists2 x, x \in G & K = (H :^ x)%G. - move=> hallK; have [sKG piK _] := and3P hallK. @@ -418,7 +418,7 @@ Proposition coprime_Hall_trans A G H1 H2 : exists2 x, x \in 'C_G(A) & H1 :=: H2 :^ x. Proof. move: H1 => H nGA coGA solG hallH nHA hallH2. -have{H2 hallH2} [x Gx -> nH1xA] := Hall_trans solG hallH2 hallH. +have{H2 hallH2} [x Gx -> nH1xA] := Hall_trans solG hallH2 hallH. have sG_AG: G \subset A <*> G by rewrite -{1}genGid genS ?subsetUr. have nG_AG: A <*> G \subset 'N(G) by rewrite gen_subG subUset nGA normG. pose N := 'N_(A <*> G)(H)%G. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index 6a8de0e..66f6156 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -306,7 +306,7 @@ Qed. Lemma acts_qact_doms (H : {group rT}) : H \subset D -> [acts A, on H | to] -> qact_dom to H :=: A. Proof. -move=> sHD aH; apply/eqP; rewrite eqEsubset; apply/andP. +move=> sHD aH; apply/eqP; rewrite eqEsubset; apply/andP. split; first exact: qact_dom_doms. apply/subsetP=> x Ax; rewrite qact_domE //; apply/gastabsP=> //. by move/gactsP: aH; move/(_ x Ax). @@ -527,11 +527,11 @@ have: K' :=: 1%G \/ K' :=: (G / H). apply/morphimP; exists (to z x) => //. suff h: qact_dom to H \subset A. by rewrite astabs_act // (subsetP aK) //; apply: (subsetP h). - by apply/subsetP=> t; rewrite qact_domE // inE; case/ andP. + by apply/subsetP=> t; rewrite qact_domE // inE; case/andP. case; last first. move/quotient_injG; rewrite !inE /=; move/(_ nKH nHG)=> c; move: nsGK. by rewrite c subxx. -rewrite /= -trivg_quotient; move=> tK'; apply:(congr1 (@gval _)); move: tK'. +rewrite /= -trivg_quotient => - tK'; apply: (congr1 (@gval _)); move: tK'. by apply: (@quotient_injG _ H); rewrite ?inE /= ?normal_refl. Qed. @@ -565,7 +565,7 @@ have aKQ1 : [acts qact_dom to N1, on K | to / N1]. have sH'N2 : H' \subset N2. rewrite /H' eHH' quotientGK ?normal_cosetpre //=. by rewrite sub_cosetpre_quo ?normal_sub. - have -> : f1 @* H' = coset N1 @* H' by rewrite f1im //=. + have -> : f1 @* H' = coset N1 @* H' by rewrite f1im //=. apply: qacts_coset => //; apply: qacts_cosetpre => //; last exact: gactsI. by apply: (subset_trans (subsetIr _ _)). have injf2 : 'injm f2. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 4255bd9..e5c2d4f 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -301,7 +301,7 @@ case: (eqsVneq P 1) => [-> | ntP] in sPhiP *. have [p_pr _ _] := pgroup_pdiv pP ntP. have [abP x1P] := abelemP p_pr Phi_quotient_abelem. apply/andP; split. - have nMP: P \subset 'N(P^`(1) <*> 'Mho^1(P)) by rewrite normsY // !gFnorm. + have nMP: P \subset 'N(P^`(1) <*> 'Mho^1(P)) by rewrite normsY // !gFnorm. rewrite -quotient_sub1 ?gFsub_trans //=. suffices <-: 'Phi(P / (P^`(1) <*> 'Mho^1(P))) = 1 by apply: morphimF. apply/eqP; rewrite (trivg_Phi (morphim_pgroup _ pP)) /= -quotientE. @@ -530,7 +530,7 @@ Lemma abelem_split_dprod rT p (A B : {group rT}) : Proof. move=> abelA sBA; have [_ cAA _]:= and3P abelA. case/splitsP: (abelem_splits abelA sBA) => C /complP[tiBC defA]. -by exists C; rewrite dprodE // (centSS _ sBA cAA) // -defA mulG_subr. +by exists C; rewrite dprodE // (centSS _ sBA cAA) // -defA mulG_subr. Qed. Lemma p_abelem_split1 rT p (A : {group rT}) x : @@ -728,8 +728,8 @@ Variables (gT : finGroupType) (p : nat) (A G : {group gT}). Lemma center_special_abelem : p.-group G -> special G -> p.-abelem 'Z(G). Proof. move=> pG [defPhi defG']. -have [-> | ntG] := eqsVneq G 1; first by rewrite center1 abelem1. -have [p_pr _ _] := pgroup_pdiv pG ntG. +have [-> | ntG] := eqsVneq G 1; first by rewrite center1 abelem1. +have [p_pr _ _] := pgroup_pdiv pG ntG. have fM: {in 'Z(G) &, {morph expgn^~ p : x y / x * y}}. by move=> x y /setIP[_ /centP cxG] /setIP[/cxG cxy _]; apply: expgMn. rewrite abelemE //= center_abelian; apply/exponentP=> /= z Zz. @@ -877,7 +877,7 @@ have [_ _ [m oZ]] := pgroup_pdiv (pgroupS sZG pG) ntZ. have lt_m1_n: m.+1 < n. suffices: 1 < logn p #|(G / 'Z(G))|. rewrite card_quotient // -divgS // logn_div ?cardSg //. - by rewrite oG oZ !pfactorK // ltn_subRL addn1. + by rewrite oG oZ !pfactorK // ltn_subRL addn1. rewrite ltnNge; apply: contra not_cGG => cycGs. apply: cyclic_center_factor_abelian; rewrite (dvdn_prime_cyclic p_pr) //. by rewrite (card_pgroup (quotient_pgroup _ pG)) (dvdn_exp2l _ cycGs). @@ -968,7 +968,7 @@ have fmG: fm @* G = 'Z(G). by apply/subsetP=> _ /morphimP[z _ Gz ->]; apply: fZ. apply/eqP; rewrite eqEsubset sfmG; apply: contraR notZx => /(prime_TIg prZ). rewrite (setIidPr _) // => fmG1; rewrite inE Gx; apply/centP=> y Gy. - by apply/commgP; rewrite -in_set1 -[[set _]]fmG1; apply: mem_morphim. + by apply/commgP; rewrite -in_set1 -[[set _]]fmG1; apply: mem_morphim. have ->: 'C_G[x] = 'ker fm. apply/setP=> z; rewrite inE (sameP cent1P commgP) !inE. by rewrite -invg_comm eq_invg_mul mulg1. @@ -1047,7 +1047,7 @@ exists [group of E]; exists [group of R] => /=. have sEG: E \subset G by rewrite join_subG !cycle_subG Gx. have [Ex Ey]: x \in E /\ y \in E by rewrite !mem_gen // inE cycle_id ?orbT. have sZE: 'Z(G) \subset E. - rewrite (('Z(G) =P E^`(1)) _) ?der_sub // eqEsubset -{2}defG' dergS // andbT. + rewrite (('Z(G) =P E^`(1)) _) ?der_sub // eqEsubset -{2}defG' dergS // andbT. apply: contraR not_cxy => /= not_sZE'. rewrite (sameP cent1P commgP) -in_set1 -[[set 1]](prime_TIg prZ not_sZE'). by rewrite /= -defG' inE !mem_commg. @@ -1290,7 +1290,7 @@ have [y Ey not_cxy]: exists2 y, y \in E & y \notin 'C[x]. by apply/subsetPn; rewrite sub_cent1; rewrite inE Ex in notZx. have notZy: y \notin 'Z(E). apply: contra not_cxy; rewrite inE Ey; apply: subsetP. - by rewrite -cent_set1 centS ?sub1set. + by rewrite -cent_set1 centS ?sub1set. pose K := 'C_E[y]; have maxK: maximal K E by apply: cent1_extraspecial_maximal. have nsKE: K <| E := p_maximal_normal pE maxK; have [sKE nKE] := andP nsKE. have oK: #|K| = (p ^ 2)%N. @@ -1440,7 +1440,7 @@ rewrite {pCGZ}(OhmE 1 pCGZ) gen_subG; apply/subsetP=> x; rewrite 3!inE -andbA. rewrite -!cycle_subG => /and3P[sXG cZX xp1] /=; have cXX := cycle_abelian x. have nZX := cents_norm cZX; have{nAG} nAX := subset_trans sXG nAG. pose XA := <[x]> <*> A; pose C := 'C(<[x]> / Z | 'Q); pose CA := A :&: C. -pose Y := <[x]> <*> CA; pose W := 'Ohm_1(Y). +pose Y := <[x]> <*> CA; pose W := 'Ohm_1(Y). have sXC: <[x]> \subset C by rewrite sub_astabQ nZX (quotient_cents _ cXX). have defY : Y = <[x]> * CA by rewrite -norm_joinEl // normsI ?nAX ?normsG. have{nAX} defXA: XA = <[x]> * A := norm_joinEl nAX. @@ -1450,7 +1450,7 @@ suffices{sXC}: XA \subset Y. have sZCA: Z \subset CA by rewrite subsetI sZA [C]astabQ sub_cosetpre. have cZCA: CA \subset 'C(Z) by rewrite subIset 1?(sub_abelian_cent2 cAA). have sZY: Z \subset Y by rewrite (subset_trans sZCA) ?joing_subr. -have{cZCA cZX} cZY: Y \subset 'C(Z) by rewrite join_subG cZX. +have{cZCA cZX} cZY: Y \subset 'C(Z) by rewrite join_subG cZX. have{cXX nZX} sY'Z : Y^`(1) \subset Z. rewrite der1_min ?cents_norm //= -/Y defY quotientMl // abelianM /= -/Z -/CA. rewrite !quotient_abelian // ?(abelianS _ cAA) ?subsetIl //=. @@ -1488,7 +1488,7 @@ Lemma Ohm1_cent_max_normal_abelem Z : odd p -> p.-group G -> [max Z | Z <| G & p.-abelem Z] -> 'Ohm_1('C_G(Z)) = Z. Proof. move=> p_odd pG; set X := 'Ohm_1('C_G(Z)). -case/maxgroupP=> /andP[nsZG abelZ] maxZ. +case/maxgroupP=> /andP[nsZG abelZ] maxZ. have [sZG nZG] := andP nsZG; have [_ cZZ expZp] := and3P abelZ. have{nZG} nsXG: X <| G by rewrite gFnormal_trans ?norm_normalI ?norms_cent. have cZX : X \subset 'C(Z) by apply/gFsub_trans/subsetIr. @@ -1549,7 +1549,7 @@ have{genXp minU xp1 sVU ltVU} expVp: exponent V %| p. apply/bigcupsP=> z _; apply/subsetP=> v Vv. by rewrite inE -order_dvdn (dvdn_trans (order_dvdG Vv)) // cardJg order_dvdn. have{A pA defA1 sX'A V expVp} Zxy: [~ x, y] \in Z. - rewrite -defA1 (OhmE 1 pA) mem_gen // !inE (exponentP expVp). + rewrite -defA1 (OhmE 1 pA) mem_gen // !inE (exponentP expVp). by rewrite (subsetP sX'A) //= mem_commg ?(subsetP sUX). by rewrite groupMl -1?[x^-1]conjg1 mem_gen // mem_imset2 // ?groupV cycle_id. have{Zxy sUX cZX} cXYxy: [~ x, y] \in 'C(XY). @@ -1610,7 +1610,7 @@ Lemma critical_p_stab_Aut H : Proof. move=> [chH sPhiZ sRZ eqCZ] pG; have sHG := char_sub chH. pose G' := (sdpair1 [Aut G] @* G)%G; pose H' := (sdpair1 [Aut G] @* H)%G. -apply/pgroupP=> q pr_q; case/Cauchy=>//= f cHF; move: (cHF);rewrite astab_ract. +apply/pgroupP=> q pr_q; case/Cauchy=> //= f cHF; move: (cHF); rewrite astab_ract. case/setIP=> Af cHFP ofq; rewrite -cycle_subG in cHF; apply: (pgroupP pG) => //. pose F' := (sdpair2 [Aut G] @* <[f]>)%G. have trHF: [~: H', F'] = 1. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index 954be43..3d9739d 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -114,7 +114,7 @@ Lemma centrals_nil (s : seq {group gT}) G : G.-central.-series 1%G s -> last 1%G s = G -> nilpotent G. Proof. move=> cGs defG; apply/forall_inP=> H /subsetIP[sHG sHR]. -move: sHG; rewrite -{}defG -subG1 -[1]/(gval 1%G). +move: sHG; rewrite -{}defG -subG1 -[1]/(gval 1%G). elim: s 1%G cGs => //= L s IHs K /andP[/and3P[sRK sKL sLG] /IHs sHL] sHs. exact: subset_trans sHR (subset_trans (commSg _ (sHL sHs)) sRK). Qed. @@ -490,7 +490,7 @@ Qed. Lemma ucn_id n G : 'Z_n('Z_n(G)) = 'Z_n(G). Proof. exact: gFid. Qed. -Lemma ucn_nilpotent n G : nilpotent 'Z_n(G). +Lemma ucn_nilpotent n G : nilpotent 'Z_n(G). Proof. by apply/ucnP; exists n; rewrite ucn_id. Qed. Lemma nil_class_ucn n G : nil_class 'Z_n(G) <= n. @@ -677,7 +677,7 @@ Lemma solvable1 : solvable [1 gT]. Proof. exact: abelian_sol (abelian1 gT). Qed. Lemma solvableS G H : H \subset G -> solvable G -> solvable H. Proof. -move=> sHG solG; apply/forall_inP=> K /subsetIP[sKH sKK']. +move=> sHG solG; apply/forall_inP=> K /subsetIP[sKH sKK']. by rewrite (forall_inP solG) // subsetI (subset_trans sKH). Qed. @@ -685,7 +685,7 @@ Lemma sol_der1_proper G H : solvable G -> H \subset G -> H :!=: 1 -> H^`(1) \proper H. Proof. move=> solG sHG ntH; rewrite properE comm_subG //; apply: implyP ntH. -by have:= forallP solG H; rewrite subsetI sHG implybNN. +by have:= forallP solG H; rewrite subsetI sHG implybNN. Qed. Lemma derivedP G : reflect (exists n, G^`(n) = 1) (solvable G). diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index f3e19b3..b595530 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -192,7 +192,7 @@ Proof. by move=> pG; rewrite -p_part part_pnat_id. Qed. Lemma properG_ltn_log p G H : p.-group G -> H \proper G -> logn p #|H| < logn p #|G|. -Proof. +Proof. move=> pG; rewrite properEneq eqEcard andbC ltnNge => /andP[sHG]. rewrite sHG /= {1}(card_pgroup pG) {1}(card_pgroup (pgroupS sHG pG)). by apply: contra; case: p {pG} => [|p] leHG; rewrite ?logn0 // leq_pexp2l. @@ -281,7 +281,7 @@ Lemma eq_in_pHall pi rho G H : {in \pi(G), pi =i rho} -> pi.-Hall(G) H = rho.-Hall(G) H. Proof. move=> eq_pi_rho; apply: andb_id2l => sHG. -congr (_ && _); apply: eq_in_pnat => p piHp. +congr (_ && _); apply: eq_in_pnat => p piHp. by apply: eq_pi_rho; apply: (piSg sHG). by congr (~~ _); apply: eq_pi_rho; apply: (pi_of_dvd (dvdn_indexg G H)). Qed. @@ -904,7 +904,7 @@ Proof. have [M maxM _]: {M | [max M | pi.-subgroup(G) M] & 1%G \subset M}. by apply: maxgroup_exists; rewrite /psubgroup sub1G pgroup1. have sOM: 'O_pi(G) \subset M by apply: bigcap_inf. -have /andP[piM sMG] := maxgroupp maxM. +have /andP[piM sMG] := maxgroupp maxM. by rewrite /psubgroup (pgroupS sOM) // (subset_trans sOM). Qed. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index 32f86f1..8925b7d 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -130,7 +130,7 @@ have trS: [transitive G, on S | 'JG]. apply/imsetP; exists P => //; apply/eqP. rewrite eqEsubset andbC acts_sub_orbit // S_P; apply/subsetP=> Q S_Q. have:= S_P; rewrite inE => /maxgroupP[/andP[_ pP]]. - have [-> max1 | ntP _] := eqVneq P 1%G. + have [-> max1 | ntP _] := eqVneq P 1%G. move/andP/max1: (S_pG _ S_Q) => Q1. by rewrite (group_inj (Q1 (sub1G Q))) orbit_refl. have:= oG_mod _ _ S_P S_P; rewrite (oG_mod _ Q) // orbit_refl. @@ -346,7 +346,7 @@ have nsHG: H :&: G <| G by rewrite /normal subsetIr normsI ?normG. rewrite -!(setIC H) defG -(partnC pi (cardG_gt0 _)). rewrite -(card_Hall (Hall_setI_normal nsHG hallR)) /= setICA. rewrite -(card_Hall (Hall_setI_normal nsHG hallK)) /= setICA. -by rewrite -defG (setIidPl (mulG_subl _ _)) (setIidPl (mulG_subr _ _)). +by rewrite -defG (setIidPl (mulG_subl _ _)) (setIidPl (mulG_subr _ _)). Qed. End SomeHall. @@ -550,7 +550,7 @@ Lemma normal_pgroup r P N : Proof. elim: r gT P N => [|r IHr] gTr P N pP nNP le_r. by exists (1%G : {group gTr}); rewrite sub1G normal1 cards1. -have [NZ_1 | ntNZ] := eqVneq (N :&: 'Z(P)) 1. +have [NZ_1 | ntNZ] := eqVneq (N :&: 'Z(P)) 1. by rewrite (TI_center_nil (pgroup_nil pP)) // cards1 logn1 in le_r. have: p.-group (N :&: 'Z(P)) by apply: pgroupS pP; rewrite /= setICA subsetIl. case/pgroup_pdiv=> // p_pr /Cauchy[// | z]. @@ -622,7 +622,7 @@ have{n leGn IHn nDG} pN: p.-group <<'N_E(D)>>. by rewrite subsetI nDG andbF. - by rewrite inE Nx1 (subsetP sEG) ?mem_gen. have Ex1y: x1 ^ y \in E. - by rewrite -mem_conjgV (normsP nEG) // groupV; case/setIP: Ny. + by rewrite -mem_conjgV (normsP nEG) // groupV; case/setIP: Ny. apply: pgroupS (genS _) (pE _ _ Ex1 Ex1y). by apply/subsetP=> u; rewrite !inE. have [y1 Ny1 Py1]: exists2 y1, y1 \in 'N_E(D) & y1 \notin P. |