mathlib3

5b828414 - feat(algebraic_topology/dold_kan): starting the definition of the counit isomorphism of the Dold-Kan equivalence (#17619)

feat(algebraic_topology/dold_kan): starting the definition of the counit isomorphism of the Dold-Kan equivalence (#17619) This PR constructs a natural isomorphism `N₁Γ₀ : Γ₀ ⋙ N₁ ≅ to_karoubi (chain_complex C ℕ)`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>