Mathbin -> Mathlib; add import to Mathlib.lean

leanprover-community · Dec 23, 2022 · b3dc815 · b3dc815
1 parent c4a5385
commit b3dc815
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -380,6 +380,7 @@ import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Order.Compare
 import Mathlib.Order.CompleteBooleanAlgebra
 import Mathlib.Order.CompleteLattice
+import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.Directed
 import Mathlib.Order.Disjoint
 import Mathlib.Order.GaloisConnection

diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
@@ -8,10 +8,10 @@ Authors: Sébastien Gouëzel
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.Order.Bounds.Basic
-import Mathbin.Order.WellFounded
-import Mathbin.Data.Set.Intervals.Basic
-import Mathbin.Data.Set.Lattice
+import Mathlib.Order.Bounds.Basic
+import Mathlib.Order.WellFounded
+import Mathlib.Data.Set.Intervals.Basic
+import Mathlib.Data.Set.Lattice
 
 /-!
 # Theory of conditionally complete lattices.