diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/center.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/commutator.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index 615e0ac..7b1aed7 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -200,7 +200,7 @@ Proof. move=> cHK; apply/setP=> z; rewrite {3}/center centM !inE. have cKH: H \subset 'C(K) by rewrite centsC. apply/imset2P/and3P=> [[x y /setIP[Hx cHx] /setIP[Ky cKy] ->{z}]| []]. - by rewrite mem_imset2 ?groupM // ?(subsetP cHK) ?(subsetP cKH). + by rewrite imset2_f ?groupM // ?(subsetP cHK) ?(subsetP cKH). case/imset2P=> x y Hx Ky ->{z}. rewrite groupMr => [cHx|]; last exact: subsetP Ky. rewrite groupMl => [cKy|]; last exact: subsetP Hx. diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index a1ffb65..904c4e9 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -181,7 +181,7 @@ Lemma commg_subr G H : ([~: G, H] \subset H) = (G \subset 'N(H)). Proof. rewrite gen_subG; apply/subsetP/subsetP=> [sRH x Gx | nGH xy]. rewrite inE; apply/subsetP=> _ /imsetP[y Ky ->]. - by rewrite conjg_Rmul groupMr // sRH // mem_imset2 ?groupV. + by rewrite conjg_Rmul groupMr // sRH // imset2_f ?groupV. case/imset2P=> x y Gx Hy ->{xy}. by rewrite commgEr groupMr // memJ_norm (groupV, nGH). Qed. @@ -254,7 +254,7 @@ Proof. have R_C := sameP trivgP commG1P. rewrite -subG1 R_C gen_subG -{}R_C gen_subG. apply: (iffP subsetP) => [cABC x y z Ax By Cz | cABC xyz]. - by apply/set1P; rewrite cABC // !mem_imset2. + by apply/set1P; rewrite cABC // !imset2_f. by case/imset2P=> _ z /imset2P[x y Ax By ->] Cz ->; rewrite cABC. Qed. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index 4733b55..334255e 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -131,7 +131,7 @@ Lemma cycleM a b : Proof. move=> cab co_ab; apply/eqP; rewrite eqEsubset -(cent_joinEl (cents_cycle cab)). rewrite join_subG {3}cab !cycleMsub // 1?coprime_sym //. -by rewrite -genM_join cycle_subG mem_gen // mem_imset2 ?cycle_id. +by rewrite -genM_join cycle_subG mem_gen // imset2_f ?cycle_id. Qed. Lemma cyclicM A B : diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 5af62c9..3786cff 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -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 //. |