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/alt.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/solvable/alt.v')
| -rw-r--r-- | mathcomp/solvable/alt.v | 4 |
1 files changed, 2 insertions, 2 deletions
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]. |