mathlib

5f68029a - feat(algebraic_topology/dold_kan): the counit isomorphism of the Dold-Kan equivalence (#17633)

feat(algebraic_topology/dold_kan): the counit isomorphism of the Dold-Kan equivalence (#17633) This PR constructs the counit isomorphism `N₂Γ₂ : Γ₂ ⋙ N₂ ≅ 𝟭 (karoubi (chain_complex C ℕ))` of the Dold-Kan equivalence.