Ulrik Buchholtz
|
0c4baacfcc
|
fix free_abelian_group and direct_sum
|
2018-11-02 13:39:40 +01:00 |
|
Ulrik Buchholtz
|
8f998637b5
|
factor free group on set via free group on pointed set
|
2018-10-23 13:30:26 +02:00 |
|
Floris van Doorn
|
68345f75ce
|
move more and update after changes
|
2018-09-11 19:24:51 +02:00 |
|
Floris van Doorn
|
ec5b9dba12
|
more on decidable free group
|
2018-06-06 16:40:41 -04:00 |
|
Floris van Doorn
|
12f23c0dbe
|
the free group on a decidable set eliminates to any InfGroup
Also develop more group theory for InfGroups
|
2018-03-25 16:51:23 -04:00 |
|
Floris van Doorn
|
aa191493e9
|
give alternative definition of free group on a set with decidable equality
|
2018-01-17 19:18:13 -05:00 |
|
Floris van Doorn
|
c19c885de3
|
fix [unfold] index
|
2017-06-07 09:40:46 -06:00 |
|
Floris van Doorn
|
984d564cc6
|
unbundle set in direct_sum
|
2017-06-07 11:30:09 -04:00 |
|
Floris van Doorn
|
c0b7740f13
|
order of arguments in group.mk has changed
|
2017-02-02 17:16:14 -05:00 |
|
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 |
|