mathlib3

24f5150e - feat(algebraic_topology/dold_kan): very basic defs for split simplicial objects in preadditive categories (#16888)

feat(algebraic_topology/dold_kan): very basic defs for split simplicial objects in preadditive categories (#16888) This PR introduces very basic definitions for split simplicial objects in preadditive category, mostly the projections `s.π_summand A` on a summand (with index `A`) in the coproduct decomposition given by `s : splitting X` where `X` is a simplicial object.