diff options
| -rw-r--r-- | mathcomp/character/vcharacter.v | 2 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 6 | ||||
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 4 | ||||
| -rw-r--r-- | mathcomp/fingroup/morphism.v | 6 | ||||
| -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 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 7 |
9 files changed, 19 insertions, 16 deletions
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index faecc02..e1c7ec4 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -696,7 +696,7 @@ have [j def_chi_j]: {j | 'chi_j = phi}. exists j; rewrite ?cfkerEirr def_chi_j //; apply/subsetP => x /setDP[Gx notHx]. rewrite inE cfunE def_phi // cfunE -/a cfun1E // Gx mulr1 cfIndE //. rewrite big1 ?mulr0 ?add0r // => y Gy; apply/theta0/(contra _ notHx) => Hxy. -by rewrite -(conjgK y x) cover_imset -class_supportEr mem_imset2 ?groupV. +by rewrite -(conjgK y x) cover_imset -class_supportEr imset2_f ?groupV. Qed. End MoreVchar. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 2a498d0..38b3490 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -1168,14 +1168,14 @@ Proof. exact: imset_f. Qed. Lemma memJ_class_support A B x y : x \in A -> y \in B -> x ^ y \in class_support A B. -Proof. by move=> Ax By; apply: mem_imset2. Qed. +Proof. by move=> Ax By; apply: imset2_f. Qed. Lemma class_supportM A B C : class_support A (B * C) = class_support (class_support A B) C. Proof. apply/setP=> x; apply/imset2P/imset2P=> [[a y Aa] | [y c]]. case/mulsgP=> b c Bb Cc -> ->{x y}. - by exists (a ^ b) c; rewrite ?(mem_imset2, conjgM). + by exists (a ^ b) c; rewrite ?(imset2_f, conjgM). case/imset2P=> a b Aa Bb -> Cc ->{x y}. by exists a (b * c); rewrite ?(mem_mulg, conjgM). Qed. @@ -2326,7 +2326,7 @@ by apply: eq_bigr => i _; rewrite genGidG. Qed. Lemma mem_commg A B x y : x \in A -> y \in B -> [~ x, y] \in [~: A, B]. -Proof. by move=> Ax By; rewrite mem_gen ?mem_imset2. Qed. +Proof. by move=> Ax By; rewrite mem_gen ?imset2_f. Qed. Lemma commSg A B C : A \subset B -> [~: A, C] \subset [~: B, C]. Proof. by move=> sAC; rewrite genS ?imset2S. Qed. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index b1181c0..7e14ce0 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -1369,7 +1369,7 @@ move=> sAH sBK; rewrite [f @* _]morphimEsub /=; last first. by rewrite norm_joinEr // mulgSS. apply/setP=> y; apply/imsetP/idP=> [[_ /mulsgP[x a Ax Ba ->] ->{y}] |]. have Hx := subsetP sAH x Ax; have Ka := subsetP sBK a Ba. - by rewrite pprodmE // mem_imset2 ?mem_morphim. + by rewrite pprodmE // imset2_f ?mem_morphim. case/mulsgP=> _ _ /morphimP[x Hx Ax ->] /morphimP[a Ka Ba ->] ->{y}. by exists (x * a); rewrite ?mem_mulg ?pprodmE. Qed. @@ -1391,7 +1391,7 @@ apply/andP/imset2P=> [[/mulsgP[x a Hx Ka ->{y}]]|[x a Hx]]. rewrite pprodmE // => fxa1. by exists x a^-1; rewrite ?invgK // inE groupVr ?morphV // eq_mulgV1 invgK. case/setIdP=> Kx /eqP fx ->{y}. -by rewrite mem_imset2 ?pprodmE ?groupV ?morphV // fx mulgV. +by rewrite imset2_f ?pprodmE ?groupV ?morphV // fx mulgV. Qed. Lemma injm_pprodm : diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 3530b35..ac4aaa7 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -290,7 +290,7 @@ Proof. move=> sAD; rewrite /morphim setIC -group_modl // (setIidPr sAD). apply/setP=> fxy; apply/idP/idP. case/imsetP=> _ /imset2P[x y Ax /setIP[Dy By] ->] ->{fxy}. - by rewrite morphM // (subsetP sAD, mem_imset2) // imset_f // inE By. + by rewrite morphM // (subsetP sAD, imset2_f) // imset_f // inE By. case/imset2P=> _ _ /imsetP[x Ax ->] /morphimP[y Dy By ->] ->{fxy}. by rewrite -morphM // (subsetP sAD, imset_f) // mem_mulg // inE By. Qed. @@ -307,7 +307,7 @@ Proof. move=> sRfD; apply/setP=> x; rewrite !inE. apply/andP/imset2P=> [[Dx] | [y z]]; last first. rewrite !inE => /andP[Dy Rfy] /andP[Dz Rfz] ->. - by rewrite ?(groupM, morphM, mem_imset2). + by rewrite ?(groupM, morphM, imset2_f). case/imset2P=> fy fz Rfy Rfz def_fx. have /morphimP[y Dy _ def_fy]: fy \in f @* D := subsetP sRfD fy Rfy. exists y (y^-1 * x); last by rewrite mulKVg. @@ -610,7 +610,7 @@ apply/setP=> fz; apply/morphimP/imset2P=> [[z _] | [fx fy]]. have Dx := sAD x Ax; have Dy := sBD y By. by exists (f x) (f y); rewrite ?(imset_f, morphR) // ?(inE, Dx, Dy). case/morphimP=> x Dx Ax ->{fx}; case/morphimP=> y Dy By ->{fy} -> {fz}. -by exists [~ x, y]; rewrite ?(inE, morphR, groupR, mem_imset2). +by exists [~ x, y]; rewrite ?(inE, morphR, groupR, imset2_f). Qed. Lemma morphim_norm A : f @* 'N(A) \subset 'N(f @* A). 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 //. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 5be507f..d6662b4 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -1264,7 +1264,7 @@ apply/setP => y. by apply/imsetP/set1P=> [[x' /set1P-> //]| ->]; exists x; rewrite ?set11. Qed. -Lemma mem_imset2 (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 : +Lemma imset2_f (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 : x \in D -> x2 \in D2 x -> f2 x x2 \in imset2 f2 (mem D) (fun x1 => mem (D2 x1)). Proof. by move=> Dx Dx2; apply/imset2P; exists x x2. Qed. @@ -2382,4 +2382,7 @@ End Greatest. End SetFixpoint. -Notation mem_imset := ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _). +Notation mem_imset := + ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _). +Notation mem_imset2 := ((fun aT aT2 rT D D2 x x2 f xD xD2 => + deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _). |