feat: port Data.Set.Prod (#1004)

fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e - [x] depends on: #1000 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
leanprover-community · Dec 14, 2022 · a5d78c3 · a5d78c3
1 parent 4f850b6
commit a5d78c3
Show file tree

Hide file tree

Showing 2 changed files with 892 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -217,6 +217,7 @@ import Mathlib.Data.Set.BoolIndicator
 import Mathlib.Data.Set.Image
 import Mathlib.Data.Set.NAry
 import Mathlib.Data.Set.Opposite
+import Mathlib.Data.Set.Prod
 import Mathlib.Data.Set.Sigma
 import Mathlib.Data.SetLike.Basic
 import Mathlib.Data.Sigma.Basic