diff options
Diffstat (limited to 'mathcomp/solvable/center.v')
| -rw-r--r-- | mathcomp/solvable/center.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index 615e0ac..7b1aed7 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -200,7 +200,7 @@ Proof. move=> cHK; apply/setP=> z; rewrite {3}/center centM !inE. have cKH: H \subset 'C(K) by rewrite centsC. apply/imset2P/and3P=> [[x y /setIP[Hx cHx] /setIP[Ky cKy] ->{z}]| []]. - by rewrite mem_imset2 ?groupM // ?(subsetP cHK) ?(subsetP cKH). + by rewrite imset2_f ?groupM // ?(subsetP cHK) ?(subsetP cKH). case/imset2P=> x y Hx Ky ->{z}. rewrite groupMr => [cHx|]; last exact: subsetP Ky. rewrite groupMl => [cKy|]; last exact: subsetP Hx. |