From c571859da2f385b8e20116456c271e57dd3dc359 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 27 Oct 2022 10:47:00 +0000 Subject: [PATCH] chore(order/bounded_order): remove unnecessary imports (#17180) Co-authored-by: Scott Morrison --- src/order/bounded_order.lean | 2 +- src/order/symm_diff.lean | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/order/bounded_order.lean b/src/order/bounded_order.lean index c8bff9fdc03e3..a7c42e6ec2d51 100644 --- 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 index a5036c065ea86..5372a68be17d0 100644 --- 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