feat(analysis/convex/topology): minimize import (#16052)

Importing `analysis/normed_space/finite_dimension` was problematic for defining the strong operator topology because this needs quite a few facts about convexity but it has to be defined before `continuous_linear_map.has_op_norm`.
leanprover-community · Aug 15, 2022 · 8df20db · 8df20db
1 parent 4a379da
commit 8df20db
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/analysis/convex/strict_convex_space.lean b/src/analysis/convex/strict_convex_space.lean
@@ -7,6 +7,7 @@ import analysis.convex.strict
 import analysis.convex.topology
 import analysis.normed_space.ordered
 import analysis.normed_space.pointwise
+import analysis.normed_space.affine_isometry
 
 /-!
 # Strictly convex spaces

diff --git a/src/analysis/convex/topology.lean b/src/analysis/convex/topology.lean
@@ -5,7 +5,7 @@ Authors: Alexander Bentkamp, Yury Kudryashov
 -/
 import analysis.convex.jensen
 import analysis.normed.group.pointwise
-import analysis.normed_space.finite_dimension
+import topology.algebra.module.finite_dimension
 import analysis.normed_space.ray
 import topology.path_connected
 import topology.algebra.affine