chore(order/filter): move filter.prod and filter.coprod to a new …

…file (#15937) These lemmas and definitions are moved without changes.
leanprover-community · Aug 9, 2022 · a913b9b · a913b9b
1 parent e71c115
commit a913b9b
Show file tree

Hide file tree

Showing 4 changed files with 423 additions and 397 deletions.
diff --git a/src/order/filter/bases.lean b/src/order/filter/bases.lean
@@ -5,7 +5,7 @@ Authors: Yury Kudryashov, Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
 import data.prod.pprod
 import data.set.countable
-import order.filter.basic
+import order.filter.prod
 
 /-!
 # Filter bases