mathlib3

421b9bbe - feat(algebraic_topology): alternating face map complex of a simplicial object (#10927)

feat(algebraic_topology): alternating face map complex of a simplicial object (#10927) added the alternating face map complex of a simplicial object in a preadditive category and the natural inclusion of the normalized_Moore_complex Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>