Move LinearMap.polar_AbsConvex into Analysis/LocallyConvex/Bipolar

mans0954 · mans0954 · commit eb6e4bdef619 · 2025-04-09T08:40:27.000+01:00
diff --git a/Mathlib/Analysis/LocallyConvex/Bipolar.lean b/Mathlib/Analysis/LocallyConvex/Bipolar.lean
@@ -9,6 +9,7 @@ import Mathlib.Analysis.LocallyConvex.AbsConvex
 import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
 import Mathlib.Analysis.LocallyConvex.WeakDual
 import Mathlib.Analysis.Normed.Module.Dual
+import Mathlib.Analysis.Normed.Module.Convex
 
 /-!
 
@@ -20,6 +21,24 @@ variable {𝕜 E F : Type*}
 
 namespace LinearMap
 
+section NormedField
+
+variable {𝕜 E F : Type*}
+variable [NormedField 𝕜] [NormedSpace ℝ 𝕜] [AddCommMonoid E] [AddCommMonoid F]
+variable [Module 𝕜 E] [Module 𝕜 F]
+
+variable {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E)
+
+variable [Module ℝ F] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 𝕜]
+
+theorem polar_AbsConvex : AbsConvex 𝕜 (B.polar s) := by
+  rw [polar_eq_biInter_preimage]
+  exact AbsConvex.iInter₂ fun i hi =>
+    ⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F →ₑ[(RingHom.id 𝕜)] 𝕜))),
+      (convex_closedBall _ _).linear_preimage (B i)⟩
+
+end NormedField
+
 
 -- `RCLike 𝕜` and `IsScalarTower ℝ 𝕜 E` needed for `RCLike.geometric_hahn_banach_closed_point`
 variable [RCLike 𝕜] [AddCommGroup E] [AddCommGroup F]
diff --git a/Mathlib/Analysis/Normed/Module/Dual.lean b/Mathlib/Analysis/Normed/Module/Dual.lean
@@ -7,8 +7,6 @@ import Mathlib.Analysis.LocallyConvex.Polar
 import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
 import Mathlib.Analysis.NormedSpace.RCLike
 import Mathlib.Data.Set.Finite.Lemmas
-import Mathlib.Analysis.LocallyConvex.AbsConvex
-import Mathlib.Analysis.Normed.Module.Convex
 
 /-!
 # The topological dual of a normed space
@@ -300,25 +298,3 @@ theorem sInter_polar_eq_closedBall {𝕜 E : Type*} [RCLike 𝕜] [NormedAddComm
 end PolarSets
 
 end NormedSpace
-
-namespace LinearMap
-
-section NormedField
-
-variable {𝕜 E F : Type*}
-variable [NormedField 𝕜] [NormedSpace ℝ 𝕜] [AddCommMonoid E] [AddCommMonoid F]
-variable [Module 𝕜 E] [Module 𝕜 F]
-
-variable {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (s : Set E)
-
-variable [Module ℝ F] [IsScalarTower ℝ 𝕜 F] [IsScalarTower ℝ 𝕜 𝕜]
-
-theorem polar_AbsConvex : AbsConvex 𝕜 (B.polar s) := by
-  rw [polar_eq_biInter_preimage]
-  exact AbsConvex.iInter₂ fun i hi =>
-    ⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F →ₑ[(RingHom.id 𝕜)] 𝕜))),
-      (convex_closedBall _ _).linear_preimage (B i)⟩
-
-end NormedField
-
-end LinearMap
