We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 8eed07a commit c6ba537Copy full SHA for c6ba537
1 file changed
Mathlib/Analysis/LocallyConvex/Separation.lean
@@ -7,11 +7,9 @@ module
7
8
public import Mathlib.Analysis.Convex.Cone.Extension
9
public import Mathlib.Analysis.Convex.Gauge
10
-public import Mathlib.Analysis.Normed.Module.Convex
11
public import Mathlib.Analysis.RCLike.Extend
12
public import Mathlib.Topology.Algebra.Module.FiniteDimension
13
public import Mathlib.Topology.Algebra.Module.LocallyConvex
14
-public import Mathlib.Topology.Instances.RealVectorSpace
15
16
/-!
17
# Separation Hahn-Banach theorem
0 commit comments