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/character/classfun.v | |
| parent | 7a34bf388b368b450f20a7e10e5a3076370d2d52 (diff) | |
rename mem_imset to imset_f (with deprecation)
Diffstat (limited to 'mathcomp/character/classfun.v')
| -rw-r--r-- | mathcomp/character/classfun.v | 2 |
1 files changed, 1 insertions, 1 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. |