From 652ef70739aaabf1aa54bf5d2ea345721c4c963d Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 1 Dec 2016 14:39:10 -0500
Subject: [PATCH] some work, I guess

---
 algebra/subgroup.hlean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index c6d4640..78d66b6 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -284,6 +284,8 @@ 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 hom_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
   begin
     fapply homomorphism.mk,