rename group_basics to subgroup

This commit is contained in:
Floris van Doorn 2016-09-14 17:12:28 -04:00
parent d2f95f344f
commit 17d76bdb31
2 changed files with 1 additions and 1 deletions

View file

@ -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