feat: port CategoryTheory.Limits.Shapes.BinaryProducts (#2507)

leanprover-community · Mar 4, 2023 · 061def7 · 061def7
1 parent 13fc258
commit 061def7
Show file tree

Hide file tree

Showing 2 changed files with 1,438 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -295,6 +295,7 @@ import Mathlib.CategoryTheory.Limits.IsLimit
 import Mathlib.CategoryTheory.Limits.Preserves.Basic
 import Mathlib.CategoryTheory.Limits.Preserves.Limits
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
+import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
 import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
 import Mathlib.CategoryTheory.Limits.Shapes.Terminal