mathlib documentation

algebraic_topology.dold_kan.equivalence_additive

The Dold-Kan equivalence for additive categories.

This file defines preadditive.dold_kan.equivalence which is the equivalence of categories karoubi (simplicial_object C) ≌ karoubi (chain_complex C ℕ).