Commit 2023-08-13 15:48 c532d7b8
View on Github →feat: forward port of Mathlib.AlgebraicTopology.DoldKan.Equivalence (#6444) In this PR (which is a forward port of https://github.com/leanprover-community/mathlib/pull/17926), the Dold-Kan equivalence between simplicial objects and chain complexes in abelian categories is constructed.