feat: port AlgebraicTopology.SimplexCategory (#3286)

leanprover-community · Apr 6, 2023 · 56944fb · 56944fb
1 parent 332ff81
commit 56944fb
Show file tree

Hide file tree

Showing 3 changed files with 823 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -278,6 +278,7 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.AlgebraicTopology.DoldKan.Compatibility
+import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.Analysis.Convex.Basic
 import Mathlib.Analysis.Convex.Extreme
 import Mathlib.Analysis.Convex.Hull