diff options
| author | Christian Doczkal | 2020-09-10 17:45:57 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-09-29 11:10:31 +0200 |
| commit | 298830c5a3860c7a645df6effe7d1cc228d56150 (patch) | |
| tree | a9a97a1ba6abd46f94d5ca48ece171cc9d88df2f /mathcomp/solvable/primitive_action.v | |
| parent | 7a34bf388b368b450f20a7e10e5a3076370d2d52 (diff) | |
rename mem_imset to imset_f (with deprecation)
Diffstat (limited to 'mathcomp/solvable/primitive_action.v')
| -rw-r--r-- | mathcomp/solvable/primitive_action.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index e6016e8..80005a4 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -80,7 +80,7 @@ apply/forallP/maximal_eqP=> /= [primG | [_ maxCx] Q]. case/imsetP=> _ /imsetP[b Hb ->] ->. by rewrite !(actsP (atrans_acts trG)) //; apply: subsetP Hb. case: (atransP2 trG Sx Sy) => a Ga ->. - by exists ((to^*)%act X a); apply: mem_imset; rewrite // orbit_refl. + by exists ((to^*)%act X a); apply: imset_f; rewrite // orbit_refl. apply/trivIsetP=> _ _ /imsetP[a Ga ->] /imsetP[b Gb ->]. apply: contraR => /exists_inP[_ /imsetP[_ /imsetP[a1 Ha1 ->] ->]]. case/imsetP=> _ /imsetP[b1 Hb1 ->] /(canLR (actK _ _)) /(canLR (actK _ _)). @@ -95,7 +95,7 @@ have QX: X \in Q by rewrite pblock_mem ?defS. have toX Y a: Y \in Q -> a \in G -> to x a \in Y -> sto X a = Y. move=> QY Ga Yxa; rewrite -(contraNeq (trivIsetP tIQ Y (sto X a) _ _)) //. by rewrite (actsP actQ). - by apply/existsP; exists (to x a); rewrite /= Yxa; apply: mem_imset. + by apply/existsP; exists (to x a); rewrite /= Yxa; apply: imset_f. have defQ: Q = orbit (to^*)%act G X. apply/eqP; rewrite eqEsubset andbC acts_sub_orbit // QX. apply/subsetP=> Y QY. @@ -245,7 +245,7 @@ apply/imsetP; exists t => //. apply/setP=> u; apply/idP/imsetP=> [du | [a Ga ->{u}]]. case: (ext_t u du) => y; rewrite tr_xt. by case/imsetP=> a Ga [_ def_u]; exists a => //; apply: val_inj. -have: n_act to xt a \in dtuple_on _ S by rewrite tr_xt mem_imset. +have: n_act to xt a \in dtuple_on _ S by rewrite tr_xt imset_f. by rewrite n_act_add dtuple_on_add; case/and3P. Qed. |