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