diff options
| author | Christian Doczkal | 2020-09-10 17:45:57 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-09-29 11:10:31 +0200 |
| commit | 298830c5a3860c7a645df6effe7d1cc228d56150 (patch) | |
| tree | a9a97a1ba6abd46f94d5ca48ece171cc9d88df2f /mathcomp/solvable/hall.v | |
| parent | 7a34bf388b368b450f20a7e10e5a3076370d2d52 (diff) | |
rename mem_imset to imset_f (with deprecation)
Diffstat (limited to 'mathcomp/solvable/hall.v')
| -rw-r--r-- | mathcomp/solvable/hall.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index 6234224..119a9fc 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.v @@ -851,7 +851,7 @@ have trNPA: A :^: AG ::&: N = A :^: N. pose NG := 'N_G(P); have sNG_G : NG \subset G := subsetIl _ _. have nNGA: A \subset 'N(NG) by rewrite normsI ?norms_norm. apply/setP=> Ax; apply/setIdP/imsetP=> [[]|[x Nx ->{Ax}]]; last first. - by rewrite conj_subG //; case/setIP: Nx => AGx; rewrite mem_imset. + by rewrite conj_subG //; case/setIP: Nx => AGx; rewrite imset_f. have ->: N = A <*> NG by rewrite /N /AG !norm_joinEl // -group_modl. have coNG_A := coprimeSg sNG_G coGA; case/imsetP=> x AGx ->{Ax}. case/SchurZassenhaus_trans_actsol; rewrite ?cardJg // => y Ny /= ->. |