feat: port AlgebraicTopology.ExtraDegeneracy (#3729)

leanprover-community · Apr 29, 2023 · 1839138 · 1839138
1 parent 328f5d9
commit 1839138
Show file tree

Hide file tree

Showing 2 changed files with 427 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -318,6 +318,7 @@ import Mathlib.AlgebraicTopology.DoldKan.Notations
 import Mathlib.AlgebraicTopology.DoldKan.PInfty
 import Mathlib.AlgebraicTopology.DoldKan.Projections
 import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
+import Mathlib.AlgebraicTopology.ExtraDegeneracy
 import Mathlib.AlgebraicTopology.MooreComplex
 import Mathlib.AlgebraicTopology.Nerve
 import Mathlib.AlgebraicTopology.SimplexCategory