Commit graph

15 commits

Author SHA1 Message Date
Floris van Doorn
b08457c77f move things to the Lean library, and update after changes in the Lean library 2016-11-24 00:11:55 -05:00
Floris van Doorn
29bf3bdd8e clean-up in imports/opens of the files in the algebra folder 2016-10-13 16:02:04 -04:00
Egbert Rijke
038bbb8be3 split group_constructions into several files 2016-10-13 15:04:57 -04:00
Floris van Doorn
d8c694e113 update after changes in the HoTT library. Mostly some naming and notation changes 2016-09-23 17:16:25 -04:00
Egbert Rijke
580298d2c7 Merge branch 'master' of https://github.com/cmu-phil/Spectral 2016-09-16 02:04:08 -04:00
Egbert Rijke
392590bec8 working with Ulrik on basic group theory 2016-09-16 02:03:58 -04:00
Floris van Doorn
683a515178 progress on LES of spectrum maps 2016-09-15 17:57:33 -04:00
Floris van Doorn
2bf316e347 add the universal property of quotient as exercises 2016-09-14 17:31:52 -04:00
Floris van Doorn
17d76bdb31 rename group_basics to subgroup 2016-09-14 17:31:52 -04:00
Floris van Doorn
d2f95f344f some small changes, move aut to group_constructions 2016-09-14 17:11:44 -04:00
Floris van Doorn
65e6e062be let group_constructions import group_basics 2016-09-14 17:07:09 -04:00
Egbert Rijke
ff99c2113a kernels were already defined later. I moved them 2016-09-07 23:05:49 -04:00
Egbert Rijke
9f4436d505 some comments on the file on group_constructions 2016-09-07 22:43:50 -04:00
Egbert Rijke
4524af4ddc image of homomorphism is subgroup 2016-05-12 16:57:33 -04:00
Floris van Doorn
ba7b25d00f move files to the HoTT library and update after changes in the HoTT library 2016-04-25 19:51:17 -04:00
Renamed from group_theory/constructions.hlean (Browse further)