chore(order/bounded_order): remove unnecessary imports (#17180)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Oct 27, 2022 · c571859 · c571859
1 parent 6bc0c19
commit c571859
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/order/bounded_order.lean b/src/order/bounded_order.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import order.lattice
-import logic.equiv.basic
+import data.option.basic
 
 /-!
 # ⊤ and ⊥, bounded lattices and variants

diff --git a/src/order/symm_diff.lean b/src/order/symm_diff.lean
@@ -5,6 +5,7 @@ Authors: Adam Topaz, Bryan Gin-ge Chen, Yaël Dillies
 -/
 
 import order.boolean_algebra
+import logic.equiv.basic
 
 /-!
 # Symmetric difference and bi-implication