mathlib

5797ef5c - feat(algebraic_topology): alternating_coface_map_complex (#14588)

feat(algebraic_topology): alternating_coface_map_complex (#14588) This PR constructs the alternating coface map complex of a cosimplicial object in an additive category. This construction is dual to the alternating face map complex.