Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 01:42 07d11baa

View on Github →

feat(algebraic/dold_kan): construction of the functors N₁ and N₂ (#16003) This PR constructs two functors, including N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ) which shall be an equivalence of categories for any preadditive category C.

Estimated changes