mathlib

c2339caa - feat(algebraic_topology): map_alternating_face_map_complex (#13028)

feat(algebraic_topology): map_alternating_face_map_complex (#13028) In this PR, we obtain a compatibility `map_alternating_face_map_complex` of the construction of the alternating face map complex functor with respect to additive functors between preadditive categories.