chore: add missing file to Mathlib.lean (#16892)

leanprover-community · Sep 17, 2024 · 9801c67 · 9801c67
1 parent 9a321de
commit 9801c67
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -902,6 +902,7 @@ import Mathlib.AlgebraicTopology.Nerve
 import Mathlib.AlgebraicTopology.Quasicategory
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
+import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialObject
 import Mathlib.AlgebraicTopology.SimplicialSet
 import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal