diff options
| author | Christian Doczkal | 2020-09-10 18:15:25 +0200 |
|---|---|---|
| committer | Christian Doczkal | 2020-09-29 11:10:31 +0200 |
| commit | 5b31a9e767694ce134fdff4461a876411eba0f2d (patch) | |
| tree | 3cccd5964f214d314aca7f77a1742b9d57245ef0 /mathcomp/fingroup/morphism.v | |
| parent | 298830c5a3860c7a645df6effe7d1cc228d56150 (diff) | |
rename mem_imset2 to imset2_f (with deprecation)
Diffstat (limited to 'mathcomp/fingroup/morphism.v')
| -rw-r--r-- | mathcomp/fingroup/morphism.v | 6 |
1 files changed, 3 insertions, 3 deletions
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). |