mathlib

07d11baa - feat(algebraic/dold_kan): construction of the functors N₁ and N₂ (#16003)

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`.