Skip to content

Commit

Permalink
fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450
Browse files Browse the repository at this point in the history
)

I'm doing this because I need to have `balanced_hull_core` before `normed_space.finite_dimensional` and this little change seems to be enough for that, but I think at some point we'll need to move lemmas so that normed_spaces come as late as possible
  • Loading branch information
ADedecker committed Apr 19, 2022
1 parent ba6a985 commit 8fa3263
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/analysis/locally_convex/balanced_core_hull.lean
Expand Up @@ -3,7 +3,7 @@ Copyright (c) 2022 Moritz Doll. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Moritz Doll
-/
import analysis.seminorm
import analysis.locally_convex.basic
import order.closure

/-!
Expand Down

0 comments on commit 8fa3263

Please sign in to comment.