From 3f10379df52f7593b4187b32c08f888d0af137b1 Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:22:41 +0100
Subject: [PATCH 1/6] Rename WeakDual to WeakBilin

---
 Mathlib.lean                                                   | 3 ++-
 .../Analysis/LocallyConvex/{WeakDual.lean => WeakBilin.lean}   | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)
 rename Mathlib/Analysis/LocallyConvex/{WeakDual.lean => WeakBilin.lean} (99%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 09a2198e928739..47f0e25aeafcd3 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1963,7 +1963,7 @@ public import Mathlib.Analysis.LocallyConvex.Polar
 public import Mathlib.Analysis.LocallyConvex.SeparatingDual
 public import Mathlib.Analysis.LocallyConvex.Separation
 public import Mathlib.Analysis.LocallyConvex.StrongTopology
-public import Mathlib.Analysis.LocallyConvex.WeakDual
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 public import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 public import Mathlib.Analysis.LocallyConvex.WeakSpace
 public import Mathlib.Analysis.LocallyConvex.WithSeminorms
@@ -7240,6 +7240,7 @@ public import Mathlib.Topology.Algebra.Module.TransferInstance
 public import Mathlib.Topology.Algebra.Module.UniformConvergence
 public import Mathlib.Topology.Algebra.Module.WeakBilin
 public import Mathlib.Topology.Algebra.Module.WeakDual
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 public import Mathlib.Topology.Algebra.Monoid
 public import Mathlib.Topology.Algebra.Monoid.AddChar
 public import Mathlib.Topology.Algebra.Monoid.Defs
diff --git a/Mathlib/Analysis/LocallyConvex/WeakDual.lean b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
similarity index 99%
rename from Mathlib/Analysis/LocallyConvex/WeakDual.lean
rename to Mathlib/Analysis/LocallyConvex/WeakBilin.lean
index f42be09aeb6c1f..4115f172d9f150 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakDual.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
@@ -12,7 +12,7 @@ public import Mathlib.LinearAlgebra.Finsupp.Span
 public import Mathlib.Topology.Algebra.Module.WeakBilin
 
 /-!
-# Weak Dual in Topological Vector Spaces
+# Weak Bilinear Topologies in Topological Vector Spaces
 
 We prove that the weak topology induced by a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` is locally
 convex and we explicitly give a neighborhood basis in terms of the family of seminorms

From 35104dbf50a2ef3a36748c032d7a94cde1ac54b2 Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:24:12 +0100
Subject: [PATCH 2/6] Add seminorms

---
 Mathlib/Analysis/LocallyConvex/WeakSpace.lean | 50 +++++++++++++++++--
 1 file changed, 45 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Analysis/LocallyConvex/WeakSpace.lean b/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
index a20819b1f86a82..9d2afe956a9fe6 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakSpace.lean
@@ -1,17 +1,26 @@
 /-
 Copyright (c) 2024 Jireh Loreaux. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jireh Loreaux
+Authors: Jireh Loreaux, Michał Świętek
 -/
 module
 
 public import Mathlib.Analysis.LocallyConvex.Separation
+public import Mathlib.Analysis.LocallyConvex.WeakBilin
 public import Mathlib.LinearAlgebra.Dual.Defs
-public import Mathlib.Topology.Algebra.Module.WeakDual
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 
-/-! # Closures of convex sets in locally convex spaces
+/-! # Weak topology on normed spaces: seminorm family and convex closures
 
-This file contains the standard result that if `E` is a vector space with two locally convex
+## Seminorm family
+
+The weak topology on `WeakSpace 𝕜 E` is generated by the seminorm family `fun f x ↦ ‖f x‖`
+indexed by `StrongDual 𝕜 E`. This follows from the general `LinearMap.weakBilin_withSeminorms`
+applied to the flipped `topDualPairing`.
+
+## Closures of convex sets
+
+This file also contains the standard result that if `E` is a vector space with two locally convex
 topologies, then the closure of a convex set is the same in either topology, provided they have the
 same collection of continuous linear functionals. In particular, the weak closure of a convex set
 in a locally convex space coincides with the closure in the original topology.
@@ -19,7 +28,38 @@ Of course, we phrase this in terms of linear maps between locally convex spaces,
 creating two separate topologies on the same space.
 -/
 
-public section
+@[expose] public section
+
+section Seminorms
+
+variable {𝕜 : Type*} [NormedField 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E]
+  [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E]
+
+namespace WeakSpace
+
+set_option backward.isDefEq.respectTransparency false in
+variable (𝕜 E) in
+/-- The family of seminorms on `WeakSpace 𝕜 E` given by `fun f x ↦ ‖f x‖`, indexed by
+`StrongDual 𝕜 E`. This is the seminorm family associated to the weak topology via the
+flipped `topDualPairing`. -/
+def seminormFamily : SeminormFamily 𝕜 (WeakSpace 𝕜 E) (StrongDual 𝕜 E) :=
+  (topDualPairing 𝕜 E).flip.toSeminormFamily
+
+set_option backward.isDefEq.respectTransparency false in
+omit [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] in
+@[simp]
+lemma seminormFamily_apply (f : StrongDual 𝕜 E) (x : WeakSpace 𝕜 E) :
+    seminormFamily 𝕜 E f x = ‖f x‖ := rfl
+
+set_option backward.isDefEq.respectTransparency false in
+omit [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] in
+variable (𝕜 E) in
+lemma withSeminorms : WithSeminorms (seminormFamily 𝕜 E) :=
+  (topDualPairing 𝕜 E).flip.weakBilin_withSeminorms
+
+end WeakSpace
+
+end Seminorms
 
 variable {𝕜 E F : Type*}
 variable [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F]

From 17aa2d93a7b33b6b061e4fd64be4a778215e98f9 Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:24:24 +0100
Subject: [PATCH 3/6] Split weakdual

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 109 +-------------
 .../Topology/Algebra/Module/WeakSpace.lean    | 137 ++++++++++++++++++
 2 files changed, 142 insertions(+), 104 deletions(-)
 create mode 100644 Mathlib/Topology/Algebra/Module/WeakSpace.lean

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 9188ee7caf0b2d..f31c0f8c6a7153 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -8,32 +8,20 @@ module
 public import Mathlib.LinearAlgebra.BilinearMap
 public import Mathlib.Topology.Algebra.Module.LinearMap
 public import Mathlib.Topology.Algebra.Module.WeakBilin
+public import Mathlib.Topology.Algebra.Module.WeakSpace
 
 /-!
 # Weak dual topology
 
-We continue in the setting of `Mathlib/Topology/Algebra/Module/WeakBilin.lean`,
-which defines the weak topology given two vector spaces `E` and `F` over a commutative semiring
-`𝕜` and a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`. The weak topology on `E` is the coarsest topology
-such that for all `y : F` every map `fun x => B x y` is continuous.
-
-In this file, we consider two special cases.
-In the case that `F = E →L[𝕜] 𝕜` and `B` being the canonical pairing, we obtain the weak-* topology,
-`WeakDual 𝕜 E := (E →L[𝕜] 𝕜)`. Interchanging the arguments in the bilinear form yields the
-weak topology `WeakSpace 𝕜 E := E`.
+This file defines the weak-* (weak dual) topology on the continuous dual `E →L[𝕜] 𝕜`.
+It is the coarsest topology such that for all `z : E` every evaluation map
+`fun v => v z` is continuous.
 
 ## Main definitions
 
-The main definitions are the types `WeakDual 𝕜 E` and `WeakSpace 𝕜 E`,
-with the respective topology instances on it.
-
-* `WeakDual 𝕜 E` is a type synonym for `Dual 𝕜 E` (when the latter is defined): both are equal to
-  the type `E →L[𝕜] 𝕜` of continuous linear maps from a module `E` over `𝕜` to the ring `𝕜`.
+* `WeakDual 𝕜 E` is a type synonym for `E →L[𝕜] 𝕜` (equal to `Dual 𝕜 E`).
 * The instance `WeakDual.instTopologicalSpace` is the weak-* topology on `WeakDual 𝕜 E`, i.e., the
   coarsest topology making the evaluation maps at all `z : E` continuous.
-* `WeakSpace 𝕜 E` is a type synonym for `E` (when the latter is defined).
-* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the
-  coarsest topology such that all `v : dual 𝕜 E` remain continuous.
 
 ## References
 
@@ -132,82 +120,12 @@ end Ring
 
 end WeakDual
 
-/-- The weak topology is the topology coarsest topology on `E` such that all functionals
-`fun x => v x` are continuous. -/
-def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
-  WeakBilin (topDualPairing 𝕜 E).flip
-deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
-
 section Semiring
 
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
 variable [ContinuousConstSMul 𝕜 𝕜]
 variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
-namespace WeakSpace
-
-instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
-  WeakBilin.instModule' (topDualPairing 𝕜 E).flip
-
-instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
-    IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E) :=
-  WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip
-
-instance instContinuousSMul [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakSpace 𝕜 E) :=
-  WeakBilin.instContinuousSMul _
-
-variable [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F]
-
-/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with
-their weak topologies. -/
-def map (f : E →L[𝕜] F) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F :=
-  { f with
-    cont :=
-      WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) }
-
-theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
-  rfl
-
-@[simp]
-theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
-  rfl
-
-end WeakSpace
-
-variable (𝕜 E) in
-/-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
-mapping). It is a linear equivalence. -/
-def toWeakSpace : E ≃ₗ[𝕜] WeakSpace 𝕜 E := LinearEquiv.refl 𝕜 E
-
-variable (𝕜 E) in
-/-- For a topological vector space `E`, "identity mapping" `E → WeakSpace 𝕜 E` is continuous.
-This definition implements it as a continuous linear map. -/
-def toWeakSpaceCLM : E →L[𝕜] WeakSpace 𝕜 E where
-  __ := toWeakSpace 𝕜 E
-  cont := by
-    apply WeakBilin.continuous_of_continuous_eval
-    exact ContinuousLinearMap.continuous
-
-variable (𝕜 E) in
-@[simp]
-theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) :
-    toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x := by rfl
-
-theorem toWeakSpaceCLM_bijective :
-    Function.Bijective (toWeakSpaceCLM 𝕜 E) :=
-  (toWeakSpace 𝕜 E).bijective
-
-/-- The canonical map from `WeakSpace 𝕜 E` to `E` is an open map. -/
-theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
-  IsOpenMap.of_inverse (toWeakSpaceCLM 𝕜 E).cont
-    (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv
-
-/-- A set in `E` which is open in the weak topology is open. -/
-theorem WeakSpace.isOpen_of_isOpen (V : Set E)
-    (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
-  simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
-
 theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α → WeakDual 𝕜 E}
     {x : WeakDual 𝕜 E} :
     Tendsto f l (𝓝 x) ↔
@@ -215,20 +133,3 @@ theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α 
   WeakBilin.tendsto_iff_forall_eval_tendsto _ ContinuousLinearMap.coe_injective
 
 end Semiring
-
-section Ring
-
-namespace WeakSpace
-
-variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
-variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
-
-instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
-  WeakBilin.instAddCommGroup (topDualPairing 𝕜 E).flip
-
-instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
-  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
-
-end WeakSpace
-
-end Ring
diff --git a/Mathlib/Topology/Algebra/Module/WeakSpace.lean b/Mathlib/Topology/Algebra/Module/WeakSpace.lean
new file mode 100644
index 00000000000000..164511adb9363f
--- /dev/null
+++ b/Mathlib/Topology/Algebra/Module/WeakSpace.lean
@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2021 Kalle Kytölä. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kalle Kytölä, Moritz Doll
+-/
+module
+
+public import Mathlib.LinearAlgebra.BilinearMap
+public import Mathlib.Topology.Algebra.Module.LinearMap
+public import Mathlib.Topology.Algebra.Module.WeakBilin
+
+/-!
+# Weak topology
+
+This file defines the weak topology on a topological vector space `E`.
+It is the coarsest topology on `E` such that all continuous linear functionals
+`fun x => v x` for `v : E →L[𝕜] 𝕜` remain continuous.
+
+## Main definitions
+
+* `WeakSpace 𝕜 E` is a type synonym for `E`.
+* The instance `WeakSpace.instTopologicalSpace` is the weak topology on `E`, i.e., the
+  coarsest topology such that all `v : E →L[𝕜] 𝕜` remain continuous.
+* `toWeakSpace`: The canonical linear equivalence `E ≃ₗ[𝕜] WeakSpace 𝕜 E`.
+* `toWeakSpaceCLM`: The identity mapping as a continuous linear map `E →L[𝕜] WeakSpace 𝕜 E`.
+
+## References
+
+* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966]
+
+## Tags
+
+weak topology, duality
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open Filter Topology
+
+variable {α 𝕜 𝕝 E F : Type*}
+
+/-- The weak topology is the topology coarsest topology on `E` such that all functionals
+`fun x => v x` are continuous. -/
+def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
+  WeakBilin (topDualPairing 𝕜 E).flip
+deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
+
+section Semiring
+
+variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+variable [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+
+namespace WeakSpace
+
+instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
+  WeakBilin.instModule' (topDualPairing 𝕜 E).flip
+
+instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
+    IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E) :=
+  WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip
+
+instance instContinuousSMul [ContinuousSMul 𝕜 𝕜] : ContinuousSMul 𝕜 (WeakSpace 𝕜 E) :=
+  WeakBilin.instContinuousSMul _
+
+variable [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F]
+
+/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with
+their weak topologies. -/
+def map (f : E →L[𝕜] F) : WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F :=
+  { f with
+    cont :=
+      WeakBilin.continuous_of_continuous_eval _ fun l => WeakBilin.eval_continuous _ (l ∘L f) }
+
+theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
+  rfl
+
+@[simp]
+theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
+  rfl
+
+end WeakSpace
+
+variable (𝕜 E) in
+/-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
+mapping). It is a linear equivalence. -/
+def toWeakSpace : E ≃ₗ[𝕜] WeakSpace 𝕜 E := LinearEquiv.refl 𝕜 E
+
+variable (𝕜 E) in
+/-- For a topological vector space `E`, "identity mapping" `E → WeakSpace 𝕜 E` is continuous.
+This definition implements it as a continuous linear map. -/
+def toWeakSpaceCLM : E →L[𝕜] WeakSpace 𝕜 E where
+  __ := toWeakSpace 𝕜 E
+  cont := by
+    apply WeakBilin.continuous_of_continuous_eval
+    exact ContinuousLinearMap.continuous
+
+variable (𝕜 E) in
+@[simp]
+theorem toWeakSpaceCLM_eq_toWeakSpace (x : E) :
+    toWeakSpaceCLM 𝕜 E x = toWeakSpace 𝕜 E x := by rfl
+
+theorem toWeakSpaceCLM_bijective :
+    Function.Bijective (toWeakSpaceCLM 𝕜 E) :=
+  (toWeakSpace 𝕜 E).bijective
+
+/-- The canonical map from `WeakSpace 𝕜 E` to `E` is an open map. -/
+theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
+  IsOpenMap.of_inverse (toWeakSpaceCLM 𝕜 E).cont
+    (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv
+
+/-- A set in `E` which is open in the weak topology is open. -/
+theorem WeakSpace.isOpen_of_isOpen (V : Set E)
+    (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
+  simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
+
+end Semiring
+
+section Ring
+
+namespace WeakSpace
+
+variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
+
+instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
+  WeakBilin.instAddCommGroup (topDualPairing 𝕜 E).flip
+
+instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
+  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
+
+end WeakSpace
+
+end Ring

From 70aa8c42f3f969eee2cf0bbe6d69818bd99cc94f Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Mon, 23 Mar 2026 10:45:28 +0100
Subject: [PATCH 4/6] Fix comments.

---
 Mathlib/Analysis/LocallyConvex/WeakBilin.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/LocallyConvex/WeakBilin.lean b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
index 4115f172d9f150..e5dfa590ad0f20 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakBilin.lean
@@ -28,7 +28,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 
 * `LinearMap.hasBasis_weakBilin`: the seminorm balls of `B.toSeminormFamily` form a
   neighborhood basis of `0` in the weak topology.
-* `LinearMap.toSeminormFamily.withSeminorms`: the topology of a weak space is induced by the
+* `LinearMap.weakBilin_withSeminorms`: the topology of a weak space is induced by the
   family of seminorms `B.toSeminormFamily`.
 * `WeakBilin.locallyConvexSpace`: a space endowed with a weak topology is locally convex.
 * `LinearMap.rightDualEquiv`: When `B` is right-separating, `F` is linearly equivalent to the
@@ -43,7 +43,7 @@ convex and we explicitly give a neighborhood basis in terms of the family of sem
 
 ## Tags
 
-weak dual, seminorm
+weak bilinear, seminorm
 -/
 
 @[expose] public section

From 559b307e2f36d0d1a8e62454c77c8a8b4bc946fe Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Wed, 25 Mar 2026 10:57:31 +0100
Subject: [PATCH 5/6] Clear imports

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 1178f5f6331609..9bd11116d0f0c2 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.LinearAlgebra.BilinearMap
 public import Mathlib.Topology.Algebra.Module.LinearMap
 public import Mathlib.Topology.Algebra.Module.WeakBilin
-public import Mathlib.Topology.Algebra.Module.WeakSpace
 
 /-!
 # Weak dual topology

From 05e5398509dd88a9378a83a6b5ccc6985eef2e52 Mon Sep 17 00:00:00 2001
From: Michal Swietek <swietekmichal@proton.me>
Date: Sun, 5 Apr 2026 18:00:41 +0200
Subject: [PATCH 6/6] adapt to Spaces

---
 Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean b/Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean
index b3bc9eea541944..88b6429fb956e7 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/WeakSpace.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.LinearAlgebra.BilinearMap
 public import Mathlib.Topology.Algebra.Module.LinearMap
-public import Mathlib.Topology.Algebra.Module.WeakBilin
+public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
 
 /-!
 # Weak topology