From 17d76bdb317d61c91bb8b85ef86c1c9340f3e6b4 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 14 Sep 2016 17:12:28 -0400
Subject: [PATCH] rename group_basics to subgroup

---
 algebra/group_constructions.hlean              | 2 +-
 algebra/{group_basics.hlean => subgroup.hlean} | 0
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename algebra/{group_basics.hlean => subgroup.hlean} (100%)

diff --git a/algebra/group_constructions.hlean b/algebra/group_constructions.hlean
index 9d7511a..a65d1f0 100644
--- a/algebra/group_constructions.hlean
+++ b/algebra/group_constructions.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Egbert Rijke
 Constructions with groups
 -/
 
-import algebra.group_theory hit.set_quotient types.list types.sum .group_basics
+import algebra.subgroup hit.set_quotient types.list types.sum .group_basics
 
 open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function
      equiv
diff --git a/algebra/group_basics.hlean b/algebra/subgroup.hlean
similarity index 100%
rename from algebra/group_basics.hlean
rename to algebra/subgroup.hlean