diff options
Diffstat (limited to 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/action.v | 62 | ||||
| -rw-r--r-- | mathcomp/fingroup/automorphism.v | 2 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 14 | ||||
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 4 | ||||
| -rw-r--r-- | mathcomp/fingroup/morphism.v | 28 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 10 | ||||
| -rw-r--r-- | mathcomp/fingroup/quotient.v | 2 |
7 files changed, 61 insertions, 61 deletions
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 2d1b6e6..3679b75 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -298,7 +298,7 @@ Lemma setactE S a : to^* S a = [set to x a | x in S]. Proof. by []. Qed. Lemma mem_setact S a x : x \in S -> to x a \in to^* S a. -Proof. exact: mem_imset. Qed. +Proof. exact: imset_f. Qed. Lemma card_setact S a : #|to^* S a| = #|S|. Proof. by apply: card_imset; apply: act_inj. Qed. @@ -321,7 +321,7 @@ Lemma orbitP A x y : Proof. by apply: (iffP imsetP) => [] [a]; exists a. Qed. Lemma mem_orbit A x a : a \in A -> to x a \in orbit to A x. -Proof. exact: mem_imset. Qed. +Proof. exact: imset_f. Qed. Lemma afixP A x : reflect (forall a, a \in A -> to x a = x) (x \in 'Fix_to(A)). Proof. @@ -607,9 +607,9 @@ Qed. Lemma orbit1P G x : reflect (orbit to G x = [set x]) (x \in 'Fix_to(G)). Proof. apply: (iffP afixP) => [xfix | xfix a Ga]. - apply/eqP; rewrite eq_sym eqEsubset sub1set -{1}[x]act1 mem_imset //=. + apply/eqP; rewrite eq_sym eqEsubset sub1set -{1}[x]act1 imset_f //=. by apply/subsetP=> y; case/imsetP=> a Ga ->; rewrite inE xfix. -by apply/set1P; rewrite -xfix mem_imset. +by apply/set1P; rewrite -xfix imset_f. Qed. Lemma card_orbit1 G x : #|orbit to G x| = 1%N -> orbit to G x = [set x]. @@ -645,9 +645,9 @@ have sXS: X \subset S := transversal_sub trXP. split=> // [x y Xx Xy /= | x Sx]. have Sx := subsetP sXS x Xx. rewrite -(inj_in_eq (pblock_inj trXP)) // eq_pblock ?defS //. - by rewrite (def_pblock tiP (mem_imset _ Sx)) ?orbit_refl. + by rewrite (def_pblock tiP (imset_f _ Sx)) ?orbit_refl. have /imsetP[y Xy defxG]: orbit to G x \in pblock P @: X. - by rewrite (pblock_transversal trXP) ?mem_imset. + by rewrite (pblock_transversal trXP) ?imset_f. suffices /orbitP[a Ga def_y]: y \in orbit to G x by exists a; rewrite ?def_y. by rewrite defxG mem_pblock defS (subsetP sXS). Qed. @@ -719,7 +719,7 @@ Lemma acts_orbit G x : G \subset D -> [acts G, on orbit to G x | to]. Proof. move/subsetP=> sGD; apply/subsetP=> a Ga; rewrite !inE sGD //. apply/subsetP=> _ /imsetP[b Gb ->]. -by rewrite inE -actMin ?sGD // mem_imset ?groupM. +by rewrite inE -actMin ?sGD // imset_f ?groupM. Qed. Lemma acts_subnorm_fix A : [acts 'N_D(A), on 'Fix_to(D :&: A) | to]. @@ -731,7 +731,7 @@ by rewrite /= (afixP Cx) // memJ_norm // groupV (subsetP (normsGI _ _) _ nAa). Qed. Lemma atrans_orbit G x : [transitive G, on orbit to G x | to]. -Proof. by apply: mem_imset; apply: orbit_refl. Qed. +Proof. by apply: imset_f; apply: orbit_refl. Qed. Section OrbitStabilizer. @@ -846,7 +846,7 @@ Lemma atrans_acts_in G S : G \subset D -> [transitive G, on S | to] -> [acts G, on S | to]. Proof. move=> sGD transG; apply/subsetP=> a Ga; rewrite !inE (subsetP sGD) //. -by apply/subsetP=> x /(atransPin sGD transG) <-; rewrite inE mem_imset. +by apply/subsetP=> x /(atransPin sGD transG) <-; rewrite inE imset_f. Qed. Lemma subgroup_transitivePin G H S x : @@ -1030,7 +1030,7 @@ Proof. by move=> GtrS x y /(atransP GtrS) <- /imsetP. Qed. Lemma atrans_acts G S : [transitive G, on S | to] -> [acts G, on S | to]. Proof. move=> GtrS; apply/subsetP=> a Ga; rewrite !inE. -by apply/subsetP=> x /(atransP GtrS) <-; rewrite inE mem_imset. +by apply/subsetP=> x /(atransP GtrS) <-; rewrite inE imset_f. Qed. Lemma atrans_supgroup G H S : @@ -1052,11 +1052,11 @@ apply/idP/andP=> [GtrS | [nSG]]. apply/andP; split=> //; apply/subsetP=> _ /imsetP[x Sx ->]. by rewrite inE (atransP GtrS). rewrite eqn_leq andbC lt0n => /andP[/existsP[X /imsetP[x Sx X_Gx]]]. -rewrite (cardD1 X) {X}X_Gx mem_imset // ltnS leqn0 => /eqP GtrS. +rewrite (cardD1 X) {X}X_Gx imset_f // ltnS leqn0 => /eqP GtrS. apply/imsetP; exists x => //; apply/eqP. rewrite eqEsubset acts_sub_orbit // Sx andbT. apply/subsetP=> y Sy; have:= card0_eq GtrS (orbit to G y). -by rewrite !inE /= mem_imset // andbT => /eqP <-; apply: orbit_refl. +by rewrite !inE /= imset_f // andbT => /eqP <-; apply: orbit_refl. Qed. Lemma atrans_dvd G S : [transitive G, on S | to] -> #|S| %| #|G|. @@ -1107,7 +1107,7 @@ have:= sHC; rewrite subsetI sub_astab1 => /andP[sHG cHx]. have Tx: x \in T by rewrite inE Sx. apply: (iffP idP) => [trN | trC]. apply/setP=> Ha; apply/setIdP/imsetP=> [[]|[a Ca ->{Ha}]]; last first. - by rewrite conj_subG //; case/setIP: Ca => Ga _; rewrite mem_imset. + by rewrite conj_subG //; case/setIP: Ca => Ga _; rewrite imset_f. case/imsetP=> a Ga ->{Ha}; rewrite subsetI !sub_conjg => /andP[_ sHCa]. have Txa: to x a^-1 \in T. by rewrite inE -sub_astab1 astab1_act actGS ?Sx ?groupV. @@ -1117,7 +1117,7 @@ apply: (iffP idP) => [trN | trC]. apply/imsetP; exists x => //; apply/setP=> y; apply/idP/idP=> [Ty|]. have [Sy cHy]:= setIP Ty; have [a Ga defy] := atransP2 trGS Sx Sy. have: H :^ a^-1 \in H :^: C. - rewrite -trC inE subsetI mem_imset 1?conj_subG ?groupV // sub_conjgV. + rewrite -trC inE subsetI imset_f 1?conj_subG ?groupV // sub_conjgV. by rewrite -astab1_act -defy sub_astab1. case/imsetP=> b /setIP[Gb /astab1P cxb] defHb. rewrite defy -{1}cxb -actM mem_orbit // inE groupM //. @@ -1267,7 +1267,7 @@ apply/setP=> a; rewrite inE in_setI; apply: andb_id2l => sDa. have [Da _] := setIP sDa; rewrite !inE Da. apply/subsetP/subsetP=> [cSa _ /imsetP[x Sx ->] | cSa x Sx]; rewrite !inE. by have:= cSa x Sx; rewrite inE -val_eqE val_subact sDa. -by have:= cSa _ (mem_imset val Sx); rewrite inE -val_eqE val_subact sDa. +by have:= cSa _ (imset_f val Sx); rewrite inE -val_eqE val_subact sDa. Qed. Lemma astabs_subact S : 'N(S | subaction) = subact_dom :&: 'N(val @: S | to). @@ -1275,8 +1275,8 @@ Proof. apply/setP=> a; rewrite inE in_setI; apply: andb_id2l => sDa. have [Da _] := setIP sDa; rewrite !inE Da. apply/subsetP/subsetP=> [nSa _ /imsetP[x Sx ->] | nSa x Sx]; rewrite !inE. - by have:= nSa x Sx; rewrite inE => /(mem_imset val); rewrite val_subact sDa. -have:= nSa _ (mem_imset val Sx); rewrite inE => /imsetP[y Sy def_y]. + by have:= nSa x Sx; rewrite inE => /(imset_f val); rewrite val_subact sDa. +have:= nSa _ (imset_f val Sx); rewrite inE => /imsetP[y Sy def_y]. by rewrite ((_ a =P y) _) // -val_eqE val_subact sDa def_y. Qed. @@ -1316,9 +1316,9 @@ Canonical quotient_action := [action of qact]. Lemma acts_qact_dom : [acts qact_dom, on 'N(H) | to]. Proof. apply/subsetP=> a nNa; rewrite !inE (astabs_dom nNa); apply/subsetP=> x Nx. -have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE mem_imset. +have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f. rewrite inE -(astabs_act _ nNa) => /rcosetsP[y Ny defHy]. -have: to x a \in H :* y by rewrite -defHy (mem_imset (to^~a)) ?rcoset_refl. +have: to x a \in H :* y by rewrite -defHy (imset_f (to^~a)) ?rcoset_refl. by apply: subsetP; rewrite mul_subG ?sub1set ?normG. Qed. @@ -1328,11 +1328,11 @@ Lemma qactEcond x a : = coset H (if a \in qact_dom then to x a else x). Proof. move=> Nx; apply: val_inj; rewrite val_subact //= qact_subdomE. -have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE mem_imset. +have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f. case nNa: (a \in _); rewrite // -(astabs_act _ nNa). rewrite !val_coset ?(acts_act acts_qact_dom nNa) //=. case/rcosetsP=> y Ny defHy; rewrite defHy; apply: rcoset_eqP. -by rewrite rcoset_sym -defHy (mem_imset (_^~_)) ?rcoset_refl. +by rewrite rcoset_sym -defHy (imset_f (_^~_)) ?rcoset_refl. Qed. Lemma qactE x a : @@ -1580,7 +1580,7 @@ Proof. move=> sAB; apply/setP=> x; rewrite !inE /morphim (setIidPr sAB). apply/subsetP/subsetP=> [cAx _ /imsetP[a Aa ->] | cfAx a Aa]. by move/cAx: Aa; rewrite !inE. -by rewrite inE; move/(_ (f a)): cfAx; rewrite inE mem_imset // => ->. +by rewrite inE; move/(_ (f a)): cfAx; rewrite inE imset_f // => ->. Qed. Lemma astab_comp S : 'C(S | comp_action) = f @*^-1 'C(S | to). @@ -2163,7 +2163,7 @@ rewrite eqEcard (card_preimset _ (act_inj _ _)) leqnn andbT. apply/subsetP=> x Nx; rewrite inE; move/(astabs_act (H :* x)): HDa. rewrite mem_rcosets mulSGid ?normG // Nx => /rcosetsP[y Ny defHy]. suffices: to x a \in H :* y by apply: subsetP; rewrite mul_subG ?sub1set ?normG. -by rewrite -defHy; apply: mem_imset; apply: rcoset_refl. +by rewrite -defHy; apply: imset_f; apply: rcoset_refl. Qed. Lemma qact_is_groupAction : is_groupAction (R / H) (to / H). @@ -2326,12 +2326,12 @@ Lemma morph_astabs : f @* 'N(S | to1) = 'N(h @: S | to2). Proof. apply/setP=> fx; apply/morphimP/idP=> [[x D1x nSx ->] | nSx]. rewrite 2!inE -{1}defD2 mem_morphim //=; apply/subsetP=> _ /imsetP[u Su ->]. - by rewrite inE -hfJ ?mem_imset // (astabs_act _ nSx). + by rewrite inE -hfJ ?imset_f // (astabs_act _ nSx). have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1). by rewrite defD2 (astabs_dom nSx). exists x => //; rewrite !inE D1x; apply/subsetP=> u Su. have /imsetP[u' Su' /injh def_u']: h (to1 u x) \in h @: S. - by rewrite hfJ // -def_fx (astabs_act _ nSx) mem_imset. + by rewrite hfJ // -def_fx (astabs_act _ nSx) imset_f. by rewrite inE def_u' ?actsDR ?(subsetP sSR). Qed. @@ -2344,13 +2344,13 @@ have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1). by rewrite defD2 (astab_dom cSx). exists x => //; rewrite !inE D1x; apply/subsetP=> u Su. rewrite inE -(inj_in_eq injh) ?actsDR ?(subsetP sSR) ?hfJ //. -by rewrite -def_fx (astab_act cSx) ?mem_imset. +by rewrite -def_fx (astab_act cSx) ?imset_f. Qed. Lemma morph_afix : h @: 'Fix_(S | to1)(A) = 'Fix_(h @: S | to2)(f @* A). Proof. apply/setP=> hu; apply/imsetP/setIP=> [[u /setIP[Su cAu] ->]|]. - split; first by rewrite mem_imset. + split; first by rewrite imset_f. by apply/afixP=> _ /morphimP[x D1x Ax ->]; rewrite -hfJ ?(afixP cAu). case=> /imsetP[u Su ->] /afixP c_hu_fA; exists u; rewrite // inE Su. apply/afixP=> x Ax; have Dx := subsetP sAD1 x Ax. @@ -2498,7 +2498,7 @@ by rewrite -groupV -{1 3}(mulg1 G) rcoset_sym -sub1set -mulGS -!rcosetE. Qed. Lemma atransR G : [transitive G, on G | 'R]. -Proof. by rewrite /atrans -{1}(mul1g G) -orbitR mem_imset. Qed. +Proof. by rewrite /atrans -{1}(mul1g G) -orbitR imset_f. Qed. Lemma faithfulR G : [faithful G, on G | 'R]. Proof. by rewrite /faithful astabR subsetIr. Qed. @@ -2555,7 +2555,7 @@ Lemma afixRs_rcosets A G : 'Fix_(rcosets G A | 'Rs)(G) = rcosets G 'N_A(G). Proof. apply/setP=> Gx; apply/setIP/rcosetsP=> [[/rcosetsP[x Ax ->]]|[x]]. by rewrite sub_afixRs_norm => Nx; exists x; rewrite // inE Ax. -by case/setIP=> Ax Nx ->; rewrite -{1}rcosetE mem_imset // sub_afixRs_norm. +by case/setIP=> Ax Nx ->; rewrite -{1}rcosetE imset_f // sub_afixRs_norm. Qed. Lemma astab1Rs G : 'C[G : {set gT} | 'Rs] = G. @@ -2669,7 +2669,7 @@ Proof. by apply: acts_sum_card_orbit; apply/actsP=> x Gx y; apply: groupJr. Qed. Lemma class_formula : \sum_(C in classes G) #|G : 'C_G[repr C]| = #|G|. Proof. rewrite -sum_card_class; apply: eq_bigr => _ /imsetP[x Gx ->]. -have: x \in x ^: G by rewrite -{1}(conjg1 x) mem_imset. +have: x \in x ^: G by rewrite -{1}(conjg1 x) imset_f. by case/mem_repr/imsetP=> y Gy ->; rewrite index_cent1 classGidl. Qed. @@ -2687,7 +2687,7 @@ rewrite -sum_card_class -sum1_card (leqif_sum cGgt0). apply/abelian_classP/forall_inP=> [cGG _ /imsetP[x Gx ->]| cGG x Gx]. by rewrite cGG ?cards1. apply/esym/eqP; rewrite eqEcard sub1set cards1 class_refl leq_eqVlt cGG //. -exact: mem_imset. +exact: imset_f. Qed. End CardClass. diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index 009e723..b9ed8e1 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -134,7 +134,7 @@ Proof. move=> x y /=; wlog Ay: x y / y \in A. by move=> IH eqfxy; case: ifP (eqfxy); [symmetry | case: ifP => //]; auto. rewrite Ay; case: ifP => [Ax | nAx def_x]; first exact: injf. -by case/negP: nAx; rewrite def_x (subsetP sBf) ?mem_imset. +by case/negP: nAx; rewrite def_x (subsetP sBf) ?imset_f. Qed. Definition perm_in := perm perm_in_inj. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index c828225..38b3490 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -1142,7 +1142,7 @@ Proof. by rewrite conjDg conjs1g. Qed. (* Classes; not much for now. *) Lemma memJ_class x y A : y \in A -> x ^ y \in x ^: A. -Proof. exact: mem_imset. Qed. +Proof. exact: imset_f. Qed. Lemma classS x A B : A \subset B -> x ^: A \subset x ^: B. Proof. exact: imsetS. Qed. @@ -1164,18 +1164,18 @@ by rewrite -[xy]invgK def_xy -conjVg; exists y. Qed. Lemma mem_classes x A : x \in A -> x ^: A \in classes A. -Proof. exact: mem_imset. Qed. +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. @@ -1376,7 +1376,7 @@ Proof. by rewrite lt0n; apply/existsP; exists (1 : gT). Qed. Lemma indexg_gt0 A : 0 < #|G : A|. Proof. rewrite lt0n; apply/existsP; exists A. -by rewrite -{2}[A]mulg1 -rcosetE; apply: mem_imset. +by rewrite -{2}[A]mulg1 -rcosetE; apply: imset_f. Qed. Lemma trivgP : reflect (G :=: 1) (G \subset [1]). @@ -1677,7 +1677,7 @@ Proof. rewrite (cardsD1 1) classes1 ltnS lt0n cards_eq0. apply/set0Pn/trivgPn=> [[xG /setD1P[nt_xG]] | [x Gx ntx]]. by case/imsetP=> x Gx def_xG; rewrite def_xG classG_eq1 in nt_xG; exists x. -by exists (x ^: G); rewrite !inE classG_eq1 ntx; apply: mem_imset. +by exists (x ^: G); rewrite !inE classG_eq1 ntx; apply: imset_f. Qed. Lemma mem_class_support A x : x \in A -> x \in class_support A G. @@ -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 ef707e1..ac4aaa7 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -223,7 +223,7 @@ Proof. by rewrite /morphim setIA setIid. Qed. Lemma morphpreIim R : f @*^-1 (f @* D :&: R) = f @*^-1 R. Proof. apply/setP=> x; rewrite morphimEdom !inE. -by case Dx: (x \in D); rewrite // mem_imset. +by case Dx: (x \in D); rewrite // imset_f. Qed. Lemma morphimIim A : f @* D :&: f @* A = f @* A. @@ -276,7 +276,7 @@ Proof. wlog suffices: A / f @* A^-1 \subset (f @* A)^-1. by move=> IH; apply/eqP; rewrite eqEsubset IH -invSg invgK -{1}(invgK A) IH. apply/subsetP=> _ /morphimP[x Dx Ax' ->]; rewrite !inE in Ax' *. -by rewrite -morphV // mem_imset // inE groupV Dx. +by rewrite -morphV // imset_f // inE groupV Dx. Qed. Lemma morphpreV R : f @*^-1 R^-1 = (f @*^-1 R)^-1. @@ -290,9 +290,9 @@ 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) // mem_imset // 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, mem_imset) // mem_mulg // inE By. +by rewrite -morphM // (subsetP sAD, imset_f) // mem_mulg // inE By. Qed. Lemma morphimMr A B : B \subset D -> f @* (A * B) = f @* A * f @* B. @@ -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. @@ -409,7 +409,7 @@ move=> sKG; apply/eqP; rewrite eqEsubset morphimI setIC. apply/subsetP=> _ /setIP[/morphimP[x Dx Ax ->] /morphimP[z Dz Gz]]. case/ker_rcoset=> {Dz}// y Ky def_x. have{z Gz y Ky def_x} Gx: x \in G by rewrite def_x groupMl // (subsetP sKG). -by rewrite mem_imset ?inE // Dx Gx Ax. +by rewrite imset_f ?inE // Dx Gx Ax. Qed. Lemma morphimIG A G : 'ker f \subset G -> f @* (A :&: G) = f @* A :&: f @* G. @@ -442,8 +442,8 @@ Qed. Lemma morphim_groupset G : group_set (f @* G). Proof. apply/group_setP; split=> [|_ _ /morphimP[x Dx Gx ->] /morphimP[y Dy Gy ->]]. - by rewrite -morph1 mem_imset ?group1. -by rewrite -morphM ?mem_imset ?inE ?groupM. + by rewrite -morph1 imset_f ?group1. +by rewrite -morphM ?imset_f ?inE ?groupM. Qed. Canonical morphpre_group fPh M := @@ -470,7 +470,7 @@ apply/idP/idP=> [/andP[Dx /morphimP[y Dy Ay eqxy]] | /imset2P[z y Kz Ay ->{x}]]. rewrite -(mulgKV y x) mem_mulg // !inE !(groupM, morphM, groupV) //. by rewrite morphV //= eqxy mulgV. have [Dy Dz]: y \in D /\ z \in D by rewrite (subsetP sAD) // dom_ker. -by rewrite groupM // morphM // mker // mul1g mem_imset // inE Dy. +by rewrite groupM // morphM // mker // mul1g imset_f // inE Dy. Qed. Lemma morphimGK G : 'ker f \subset G -> G \subset D -> f @*^-1 (f @* G) = G. @@ -608,9 +608,9 @@ rewrite morphim_gen; last first; last congr <<_>>. apply/setP=> fz; apply/morphimP/imset2P=> [[z _] | [fx fy]]. case/imset2P=> x y Ax By -> -> {z fz}. have Dx := sAD x Ax; have Dy := sBD y By. - by exists (f x) (f y); rewrite ?(mem_imset, morphR) // ?(inE, Dx, Dy). + 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). @@ -1072,7 +1072,7 @@ Qed. Lemma morphpre_factm (C : {set rT}) : ff @*^-1 C = q @* (f @*^-1 C). Proof. apply/setP=> y; rewrite !inE /=; apply/andP/morphimP=> [[]|[x Hx]]; last first. - by case/morphpreP=> Gx Cfx ->; rewrite factmE ?mem_imset ?inE ?Hx. + by case/morphpreP=> Gx Cfx ->; rewrite factmE ?imset_f ?inE ?Hx. case/morphimP=> x Hx Gx ->; rewrite factmE //. by exists x; rewrite // !inE Gx. Qed. @@ -1268,7 +1268,7 @@ apply: (iffP eqP) => [eqfGH | [injf <-]]; last first. by rewrite -injmD1 // morphimEsub ?subsetDl. split. apply/subsetP=> x /morphpreP[Gx fx1]; have: f x \notin H^# by rewrite inE fx1. - by apply: contraR => ntx; rewrite -eqfGH mem_imset // inE ntx. + by apply: contraR => ntx; rewrite -eqfGH imset_f // inE ntx. rewrite morphimEdom -{2}(setD1K (group1 G)) imsetU eqfGH. by rewrite imset_set1 morph1 setD1K. Qed. @@ -1501,7 +1501,7 @@ Lemma ker_subg : 'ker (subg G) = 1. Proof. exact/trivgP. Qed. Lemma im_subg : subg G @* G = [subg G]. Proof. apply/eqP; rewrite -subTset morphimEdom. -by apply/subsetP=> u _; rewrite -(sgvalK u) mem_imset ?subgP. +by apply/subsetP=> u _; rewrite -(sgvalK u) imset_f ?subgP. Qed. Lemma sgval_sub A : sgval @* A \subset G. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index d0ba321..ebd4230 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -351,7 +351,7 @@ Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|porbits s|. Lemma apermE x s : aperm x s = s x. Proof. by []. Qed. Lemma mem_porbit s i x : (s ^+ i) x \in porbit s x. -Proof. by rewrite (mem_imset (aperm x)) ?mem_cycle. Qed. +Proof. by rewrite (imset_f (aperm x)) ?mem_cycle. Qed. Lemma porbit_id s x : x \in porbit s x. Proof. by rewrite -{1}[x]perm1 (mem_porbit s 0). Qed. @@ -442,9 +442,9 @@ have xfC a b u: xf b a (t a b u) = xf a b u. by move/lt_xf: (lt_a); rewrite -(tXC a b) 1?ltnW //= orbC [_ || _]eq_xf. pose ts := t x y s; rewrite /= -[_ * s]/ts. pose dp u := #|porbits u :\ porbit u y :\ porbit u x|. -rewrite !(addnC #|_|) (cardsD1 (porbit ts y)) mem_imset ?inE //. -rewrite (cardsD1 (porbit ts x)) inE mem_imset ?inE //= -/(dp ts) {}/ts. -rewrite (cardsD1 (porbit s y)) (cardsD1 (porbit s x)) !(mem_imset, inE) //. +rewrite !(addnC #|_|) (cardsD1 (porbit ts y)) imset_f ?inE //. +rewrite (cardsD1 (porbit ts x)) inE imset_f ?inE //= -/(dp ts) {}/ts. +rewrite (cardsD1 (porbit s y)) (cardsD1 (porbit s x)) !(imset_f, inE) //. rewrite -/(dp s) !addnA !eq_porbit_mem andbT; congr (_ + _); last first. wlog suffices: s / dp s <= dp (t x y s). by move=> IHs; apply/eqP; rewrite eqn_leq -{2}(tK x y s) !IHs. @@ -452,7 +452,7 @@ rewrite -/(dp s) !addnA !eq_porbit_mem andbT; congr (_ + _); last first. rewrite !inE andbA andbC !(eq_sym C) => /and3P[/imsetP[z _ ->{C}]]. rewrite 2!eq_porbit_mem => sxz syz. suffices ts_z: porbit (t x y s) z = porbit s z. - by rewrite -ts_z !eq_porbit_mem {1 2}ts_z sxz syz mem_imset ?inE. + by rewrite -ts_z !eq_porbit_mem {1 2}ts_z sxz syz imset_f ?inE. suffices exp_id n: ((t x y s) ^+ n) z = (s ^+ n) z. apply/setP=> u; apply/idP/idP=> /imsetP[_ /cycleP[i ->] ->]. by rewrite /aperm exp_id mem_porbit. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index f73fda5..4fd84fb 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -301,7 +301,7 @@ Lemma quotient_setIpre A D : (A :&: coset H @*^-1 D) / H = A / H :&: D. Proof. exact: morphim_setIpre. Qed. Lemma mem_quotient x G : x \in G -> coset H x \in G / H. -Proof. by move=> Gx; rewrite -imset_coset mem_imset. Qed. +Proof. by move=> Gx; rewrite -imset_coset imset_f. Qed. Lemma quotientS A B : A \subset B -> A / H \subset B / H. Proof. exact: morphimS. Qed. |