Notations for the Dold-Kan equivalence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the notation K[X] : chain_complex C ℕ for the alternating face map complex of (X : simplicial_object C) where C is a preadditive category, as well as N[X] for the normalized subcomplex in the case C is an abelian category.

(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)