mathlib3

78dddf53 - feat(algebraic_topology/dold_kan): N₁ reflects isomorphisms (#16778)

feat(algebraic_topology/dold_kan): N₁ reflects isomorphisms (#16778) In this PR, it is shown that `N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)` reflects isomorphisms for any preadditive category `C`.