[Merged by Bors] - feat(Algebra/Homology/ShortComplex): cycles can be computed with a limit kernel fork#33874

joelriou wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

joelriou:spectral-sequences-3-shortcomplex-homologyjoelriou/mathlib4:spectral-sequences-3-shortcomplex-homologyCopy head branch name to clipboard