Spectral/algebra
2017-06-30 13:55:39 +01:00
..
arrow_group.hlean Work on the fact that pointed dependent products preserve fibration sequences 2017-06-19 02:03:54 -04:00
cogroup.hlean finish construction of exact couple from a sequence of spectrum maps 2017-05-21 00:39:53 -04:00
direct_sum.hlean Add Hpwedge. 2017-06-09 15:01:21 -06:00
exact_couple.hlean making a start on the exactness of the derived couple 2017-06-19 13:40:52 -04:00
exactness.hlean move basic lemmas from the spectral repository to the main repository 2017-06-02 12:15:31 -04:00
free_commutative_group.hlean unbundle set in direct_sum 2017-06-07 11:30:09 -04:00
free_group.hlean fix [unfold] index 2017-06-07 09:40:46 -06:00
graded.hlean remove uses of homomorphism_comp_compute 2017-06-14 22:56:03 -04:00
group_constructions.hlean move things to the Lean library, and update after changes in the Lean library 2016-11-24 00:11:55 -05:00
left_module.hlean move basic lemmas from the spectral repository to the main repository 2017-06-02 12:15:31 -04:00
module_chain_complex.hlean move basic lemmas from the spectral repository to the main repository 2017-06-02 12:15:31 -04:00
module_exact_couple.hlean add strunc file for truncatedness/truncations of spectra 2017-06-28 13:15:49 +01:00
product_group.hlean add authors of mrc projects to files with major contributions 2017-06-30 13:55:39 +01:00
quotient_group.hlean seq_colim universal property 2017-06-08 18:17:23 -04:00
seq_colim.hlean add authors of mrc projects to files with major contributions 2017-06-30 13:55:39 +01:00
serre.hlean move some stuff to more appropriate places (before big move to HoTT library) 2017-05-26 17:32:42 -04:00
ses.hlean move basic lemmas from the spectral repository to the main repository 2017-06-02 12:15:31 -04:00
short_five.hlean fixed 2017-06-30 13:21:49 +01:00
subgroup.hlean completed definition of k prime 2017-06-16 17:06:04 -04:00
submodule.hlean remove uses of homomorphism_comp_compute 2017-06-14 22:56:03 -04:00