refactor(analysis/convex/cone): move cone.lean to cone/basic.lean (#1…

…6270) Part of #16266 I intend to create another file for `proper_cone`, which for cyclic import reasons cannot be included in cone.lean. So I want to move cone.lean to cone/basic.lean and create cone/proper.lean in a separate PR.
leanprover-community · Aug 31, 2022 · d44692a · d44692a
1 parent 2d30ffc
commit d44692a
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 3 deletions.
diff --git a/src/analysis/convex/cone.lean → src/analysis/convex/cone/basic.lean b/src/analysis/convex/cone.lean → src/analysis/convex/cone/basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Yury Kudryashov All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Frédéric Dupuis
 -/
-import analysis.convex.hull
 import analysis.inner_product_space.projection
 
 /-!

diff --git a/src/analysis/normed_space/hahn_banach/extension.lean b/src/analysis/normed_space/hahn_banach/extension.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Heather Macbeth
 -/
-import analysis.convex.cone
+import analysis.convex.cone.basic
 import analysis.normed_space.is_R_or_C
 import analysis.normed_space.extend
 

diff --git a/src/analysis/normed_space/hahn_banach/separation.lean b/src/analysis/normed_space/hahn_banach/separation.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Bhavik Mehta All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Yaël Dillies
 -/
-import analysis.convex.cone
+import analysis.convex.cone.basic
 import analysis.convex.gauge
 
 /-!