mathlib

50cbd1a0 - feat(algebraic_topology/dold_kan): the normalized Moore complex of a split simplicial object (#17548)

feat(algebraic_topology/dold_kan): the normalized Moore complex of a split simplicial object (#17548) This PR constructs the chain complex of "nondegenerate simplices" of a split simplicial object and show that it is isomorphic to the normalized Moore complex. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>