mathlib

324a7502 - feat(algebraic_topology): extra degeneracies and homotopy equivalences (#16855)

feat(algebraic_topology): extra degeneracies and homotopy equivalences (#16855) In this PR, it is shown that if an augmented simplicial object `X` in a preadditive category has an extra degeneracy, then the augmentation is a homotopy equivalence on the alternating face map complex.