diff options
| author | Cyril Cohen | 2017-11-23 16:33:36 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-02-06 13:54:37 +0100 |
| commit | fafd4dac5315e1d4e071b0044a50a16360b31964 (patch) | |
| tree | 5b66c3d67e2b146e3a8013496379b96dd60dc75a /mathcomp/solvable/hall.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/solvable/hall.v')
| -rw-r--r-- | mathcomp/solvable/hall.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |