mathlib3

88bca0ce - feat(algebraic_topology/dold_kan): N₂ reflects isomorphisms (#17577)

feat(algebraic_topology/dold_kan): N₂ reflects isomorphisms (#17577) This PR shows that `N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ))` reflects isomorphisms.