From 9801c67765e45f8224d33f2d1863ab5ec08548b8 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Tue, 17 Sep 2024 14:06:26 +0000 Subject: [PATCH] chore: add missing file to `Mathlib.lean` (#16892) --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 758b666e67f85..9c380afe4ca78 100644 --- 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