feat: port CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqu…

…alizers (#2764)
leanprover-community · Mar 11, 2023 · 07ab9d6 · 07ab9d6
1 parent 2f0f752
commit 07ab9d6
Show file tree

Hide file tree

Showing 3 changed files with 510 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -316,6 +316,7 @@ import Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 import Mathlib.CategoryTheory.Limits.Constructions.Equalizers
 import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
+import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
 import Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
 import Mathlib.CategoryTheory.Limits.Creates
 import Mathlib.CategoryTheory.Limits.EssentiallySmall