diff options
| author | Cyril Cohen | 2020-09-29 13:24:57 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-29 13:24:57 +0200 |
| commit | eb47a0a031efab69f9a39c8cf356e2304c1e318f (patch) | |
| tree | 000c3c9d321c68075b672c4367805b7bbcc8ee90 /mathcomp/solvable/maximal.v | |
| parent | 5fc83c2c7610f7034e5c0e92b18093deb340995d (diff) | |
| parent | 544d89a7711be2f25c3a845130e5cede590bc766 (diff) | |
Merge pull request #592 from chdoc/mem_imset
Fix naming inconsistencies between `imset` and `map` lemmas.
Diffstat (limited to 'mathcomp/solvable/maximal.v')
| -rw-r--r-- | mathcomp/solvable/maximal.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 95b7184..3786cff 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -301,7 +301,7 @@ apply/andP; split. apply/abelemP=> //; rewrite [abelian _]quotient_cents2 ?joing_subl //. split=> // _ /morphimP[x Nx Px ->] /=. rewrite -morphX //= coset_id // (MhoE 1 pP) joing_idr expn1. - by rewrite mem_gen //; apply/setUP; right; apply: mem_imset. + by rewrite mem_gen //; apply/setUP; right; apply: imset_f. rewrite -quotient_cents2 // [_ \subset 'C(_)]abP (MhoE 1 pP) gen_subG /=. apply/subsetP=> _ /imsetP[x Px ->]; rewrite expn1. have nPhi_x: x \in 'N('Phi(P)) by apply: (subsetP nPhiP). @@ -731,7 +731,7 @@ rewrite -{1}defG' gen_subG; apply/subsetP=> _ /imset2P[x y Gx Gy ->]. have Zxy: [~ x, y] \in 'Z(G) by rewrite -defG' mem_commg. have Zxp: x ^+ p \in 'Z(G). rewrite -defPhi (Phi_joing pG) (MhoE 1 pG) joing_idr mem_gen // !inE. - by rewrite expn1 orbC (mem_imset (expgn^~ p)). + by rewrite expn1 orbC (imset_f (expgn^~ p)). rewrite mem_morphpre /= ?defG' ?Zxy // inE -commXg; last first. by red; case/setIP: Zxy => _ /centP->. by apply/commgP; red; case/setIP: Zxp => _ /centP->. @@ -1157,7 +1157,7 @@ have defS: <<X>> = S. apply: Phi_nongen; apply/eqP; rewrite eqEsubset join_subG sPS sXS -joing_idr. rewrite -genM_join sub_gen // -quotientSK ?quotient_gen // -defSb genS //. apply/subsetP=> xb Xxb; apply/imsetP; rewrite (setIidPr nPX). - by exists (repr xb); rewrite /= ?coset_reprK //; apply: mem_imset. + by exists (repr xb); rewrite /= ?coset_reprK //; apply: imset_f. pose f (a : {perm gT}) := [ffun x => if x \in X then x^-1 * a x else 1]. have injf: {in A &, injective f}. move=> _ _ /morphimP[y nSy Ry ->] /morphimP[z nSz Rz ->]. @@ -1544,7 +1544,7 @@ have{genXp minU xp1 sVU ltVU} expVp: exponent V %| p. have{A pA defA1 sX'A V expVp} Zxy: [~ x, y] \in Z. 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. + by rewrite groupMl -1?[x^-1]conjg1 mem_gen // imset2_f // ?groupV cycle_id. have{Zxy sUX cZX} cXYxy: [~ x, y] \in 'C(XY). by rewrite centsC in cZX; rewrite defXY (subsetP (centS sUX)) ?(subsetP cZX). rewrite -defU1 exponent_Ohm1_class2 // nil_class2 -defXY der1_joing_cycles //. |