feat: port CategoryTheory.Limits.Shapes.Products (#2564)

Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Mar 7, 2023 · 4037792 · 4037792
1 parent 5c5f9d7
commit 4037792
Show file tree

Hide file tree

Showing 2 changed files with 447 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -305,6 +305,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
 import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
 import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
+import Mathlib.CategoryTheory.Limits.Shapes.Products
 import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
 import Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
 import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi