Spectral/algebra
2017-06-02 12:16:07 -04:00
..
arrow_group.hlean define parametrized cohomology 2017-05-24 08:27:06 -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 move basic lemmas from the spectral repository to the main repository 2017-06-02 12:15:31 -04:00
exact_couple.hlean very small additions 2017-06-02 12:16:07 -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 checkpoint for direct sum of graded modules 2017-04-10 20:34:49 -04:00
free_group.hlean order of arguments in group.mk has changed 2017-02-02 17:16:14 -05:00
graded.hlean construct the derived couple for graded modules 2017-05-22 21:27:34 -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 move basic lemmas from the spectral repository to the main repository 2017-06-02 12:15:31 -04:00
product_group.hlean Work on the construction of exact couples 2017-05-21 00:39:53 -04:00
quotient_group.hlean move basic lemmas from the spectral repository to the main repository 2017-06-02 12:15:31 -04: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 move basic lemmas from the spectral repository to the main repository 2017-06-02 12:15:31 -04:00
subgroup.hlean very small additions 2017-06-02 12:16:07 -04:00
submodule.hlean construct the derived couple for graded modules 2017-05-22 21:27:34 -04:00