aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/solvable/center.v
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/solvable/center.v')
-rw-r--r--mathcomp/solvable/center.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index f984960..98434ba 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -187,7 +187,7 @@ End Injm.
End Center.
-Arguments center_idP [gT A].
+Arguments center_idP {gT A}.
Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) :
G \isog H -> 'Z(G) \isog 'Z(H).