mathlib

19d6240d - feat(algebraic_topology/dold-kan): The Dold-Kan equivalence for additive categories (#17640)

feat(algebraic_topology/dold-kan): The Dold-Kan equivalence for additive categories (#17640) This PR defines the Dold-Kan equivalence `karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ)` between the idempotent completions of the categories `simplicial_object C` and `chain_complex C ℕ` when `C` is an additive category.