rename mem_imset to imset_f (with deprecation)

3 files changed, 7 insertions, 7 deletions

diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 9c4557a..356ff5c 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -2355,7 +2355,7 @@ Proof.
 have [[injg defR] [injh defS]] := (isomP isoG, isomP isoH).
 rewrite !morphimEdom in defS defR; apply/cfun_inP=> s.
 rewrite -{1}defS => /imsetP[x Hx ->] {s}; have Gx := subsetP sHG x Hx.
-rewrite {1}eq_hg ?(cfResE, cfIsomE) // -defS -?eq_hg ?mem_imset // -defR.
+rewrite {1}eq_hg ?(cfResE, cfIsomE) // -defS -?eq_hg ?imset_f // -defR.
 by rewrite (eq_in_imset eq_hg) imsetS.
 Qed.
 
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 3809e73..76535fa 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -396,7 +396,7 @@ apply: (iffP imageP) => [[_ /rcosetsP[y Ay ->] ->] | [y Ay ->]].
 without loss nHy: y Ay / y \in 'N(H).
   have [nHy | /cfConjgEout->] := boolP (y \in 'N(H)); first exact.
   by move/(_ 1%g); rewrite !group1 !cfConjgJ1; apply.
-exists ('I_A[phi] :* y); first by rewrite -rcosetE mem_imset.
+exists ('I_A[phi] :* y); first by rewrite -rcosetE imset_f.
 case: repr_rcosetP => z /setIP[_ /setIdP[nHz /eqP Tz]].
 by rewrite cfConjgMnorm ?Tz.
 Qed.
@@ -467,7 +467,7 @@ Proof.
 move=> nsHG; have UchiG := cfclass_uniq 'chi_i nsHG.
 apply: uniq_perm; rewrite ?(map_inj_uniq irr_inj) ?enum_uniq // => phi.
 apply/imageP/idP=> [[j iGj ->] | /cfclassP[y]]; first by rewrite -cfclass_IirrE.
-by exists (conjg_Iirr i y); rewrite ?mem_imset ?conjg_IirrE.
+by exists (conjg_Iirr i y); rewrite ?imset_f ?conjg_IirrE.
 Qed.
 
 Lemma card_cfclass_Iirr i : H <| G -> #|cfclass_Iirr G i| = #|G : 'I_G['chi_i]|.
@@ -1560,7 +1560,7 @@ have acts_Js : [acts G, on classes K | 'Js].
   apply/subsetP=> y Gy; have nKy := subsetP nKG y Gy.
   rewrite !inE; apply/subsetP=> _ /imsetP[z Gz ->]; rewrite !inE /=.
   rewrite -class_rcoset norm_rlcoset // class_lcoset.
-  by apply: mem_imset; rewrite memJ_norm.
+  by apply: imset_f; rewrite memJ_norm.
 have acts_cto : [acts G, on classes K | cto] by rewrite astabs_ract subsetIidl.
 pose m := #|'Fix_(classes K | cto)[x]|.
 have def_m: #|'Fix_ito[x]| = m.
@@ -1573,7 +1573,7 @@ apply: contraR => notKx; apply/cards1P; exists 1%g; apply/esym/eqP.
 rewrite eqEsubset !(sub1set, inE) classes1 /= conjs1g eqxx /=.
 apply/subsetP=> _ /setIP[/imsetP[y Ky ->] /afix1P /= cyKx].
 have /imsetP[z Kz def_yx]: y ^ x \in y ^: K.
-  by rewrite -cyKx; apply: mem_imset; apply: class_refl.
+  by rewrite -cyKx; apply: imset_f; apply: class_refl.
 rewrite inE classG_eq1; apply: contraR notKx => nty.
 rewrite -(groupMr x (groupVr Kz)).
 apply: (subsetP (regK y _)); first exact/setD1P.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index 2b886a6..c603f91 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -465,9 +465,9 @@ transitivity ('chi_i x * 'chi_i (x^-1)%g *+ #|h x|); last first.
       by rewrite mulf_neq0 // lin_char_neq0 /= ?cfcenter_fful_irr.
     rewrite -[z](mulKg u) -cGz // -conjMg /h classGidl {u Gu}//.
     apply/eqP/setP=> w; apply/mulsgP/mulsgP=> [][_ z1 /imsetP[v Gv ->] Zz1 ->].
-      exists (x ^ v)%g (z * z1)%g; rewrite ?mem_imset ?groupM //.
+      exists (x ^ v)%g (z * z1)%g; rewrite ?imset_f ?groupM //.
       by rewrite conjMg -mulgA /(z ^ v)%g cGz // mulKg.
-    exists ((x * z) ^ v)%g (z^-1 * z1)%g; rewrite ?mem_imset ?groupM ?groupV //.
+    exists ((x * z) ^ v)%g (z^-1 * z1)%g; rewrite ?imset_f ?groupM ?groupV //.
     by rewrite conjMg -mulgA /(z ^ v)%g cGz // mulKg mulKVg.
   rewrite !irr_inv DchiZ ?groupJ ?cfunJ // rmorphM mulrACA -!normCK -exprMn.
   by rewrite (normC_lin_char lin_lambda) ?mulr1 //= cfcenter_fful_irr.