Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-08 20:02 324a7502

View on Github →

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.

Estimated changes