Floris van Doorn 12a9345df1 Restructure spectral sequences, compute cohomology of projective space ... This is still work in progress. Spectral sequences should be more usable, and probably the degrees of graded maps should be group homomorphisms so that we can reindex spectral sequences.		2017-11-22 16:14:07 -05:00
..
degree.hlean	define pmap in terms of ppi. Also move many facts about ppi to the standard library	2017-07-21 15:55:27 +01:00
EM.hlean	fix homotopy.EM so that it compiles	2017-09-15 19:03:14 -04:00
fwedge.hlean	define pmap in terms of ppi. Also move many facts about ppi to the standard library	2017-07-21 15:55:27 +01:00
join_theorem.hlean	make everything compile on lean post 6f74f6522...	2016-03-24 16:14:44 -04:00
pushout.hlean	add naturality of sigma's commuting with pushouts	2017-08-22 22:34:22 +01:00
realprojective.hlean	fix realprojective after sphere reindexing	2017-07-23 11:52:02 +02:00
smash.hlean	define pmap in terms of ppi. Also move many facts about ppi to the standard library	2017-07-21 15:55:27 +01:00
smash_adjoint.hlean	define pmap in terms of ppi. Also move many facts about ppi to the standard library	2017-07-21 15:55:27 +01:00
spherical_fibrations.hlean	make pointed suspension and spheres the default	2017-07-20 18:03:13 +01:00
susp.hlean	move naturality of loop-susp-adjunction to standard library	2017-07-20 18:55:51 +01:00
susp_product.hlean	move some files around, create folder cohomology	2017-07-17 13:58:36 +01:00
three_by_three.hlean	various properties of pushout: commutation with sums and sigma's	2017-08-02 23:06:16 +01:00
wedge.hlean	Restructure spectral sequences, compute cohomology of projective space	2017-11-22 16:14:07 -05:00