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/solvable/commutator.v | |
| parent | 298830c5a3860c7a645df6effe7d1cc228d56150 (diff) | |
rename mem_imset2 to imset2_f (with deprecation)
Diffstat (limited to 'mathcomp/solvable/commutator.v')
| -rw-r--r-- | mathcomp/solvable/commutator.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index a1ffb65..904c4e9 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -181,7 +181,7 @@ Lemma commg_subr G H : ([~: G, H] \subset H) = (G \subset 'N(H)). Proof. rewrite gen_subG; apply/subsetP/subsetP=> [sRH x Gx | nGH xy]. rewrite inE; apply/subsetP=> _ /imsetP[y Ky ->]. - by rewrite conjg_Rmul groupMr // sRH // mem_imset2 ?groupV. + by rewrite conjg_Rmul groupMr // sRH // imset2_f ?groupV. case/imset2P=> x y Gx Hy ->{xy}. by rewrite commgEr groupMr // memJ_norm (groupV, nGH). Qed. @@ -254,7 +254,7 @@ Proof. have R_C := sameP trivgP commG1P. rewrite -subG1 R_C gen_subG -{}R_C gen_subG. apply: (iffP subsetP) => [cABC x y z Ax By Cz | cABC xyz]. - by apply/set1P; rewrite cABC // !mem_imset2. + by apply/set1P; rewrite cABC // !imset2_f. by case/imset2P=> _ z /imset2P[x y Ax By ->] Cz ->; rewrite cABC. Qed. |