Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-10 16:28 19d6240d

View on Github →

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.

Estimated changes