From de641aac7199a1aeff6257634fa7866f1ae003d0 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Thu, 1 Dec 2016 14:41:36 -0500 Subject: [PATCH] fix --- algebra/subgroup.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index 1d00fac..08a1a32 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -284,7 +284,7 @@ namespace group definition image_incl {G H : Group} (f : G →g H) : image f →g H := incl_of_subgroup (image_subgroup f) - definition comm_image_incl {A B : CommGroup} (f : A →g B) : comm_image f →g B := incl_of_subgroup (image_subgroup f) + definition comm_image_incl {A B : AbGroup} (f : A →g B) : ab_image f →g B := incl_of_subgroup (image_subgroup f) definition hom_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K := begin