diff --git a/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean b/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
index e033d86ed22bd5..2efb0e96f5495c 100644
--- a/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
+++ b/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
@@ -648,7 +648,7 @@ protected noncomputable def supSeminorm (i : ℕ) : Seminorm 𝕜 𝓓^{n}_{K}(E
 
 protected theorem withSeminorms :
     WithSeminorms (ContDiffMapSupportedIn.seminorm 𝕜 E F n K) := by
-  let p : SeminormFamily 𝕜 𝓓^{n}_{K}(E, F) ((_ : ℕ) × Fin 1) :=
+  let p : SeminormFamily 𝕜 𝓓^{n}_{K}(E, F) ((_ : ℕ) × Unit) :=
     SeminormFamily.sigma fun i _ ↦
       (normSeminorm 𝕜 (E →ᵇ (E [×i]→L[ℝ] F))).comp (structureMapLM 𝕜 n i)
   have : WithSeminorms p :=
diff --git a/Mathlib/Analysis/Fourier/AddCircleMulti.lean b/Mathlib/Analysis/Fourier/AddCircleMulti.lean
index e141194f7ebb4a..08075cd8aa8f5e 100644
--- a/Mathlib/Analysis/Fourier/AddCircleMulti.lean
+++ b/Mathlib/Analysis/Fourier/AddCircleMulti.lean
@@ -220,7 +220,7 @@ theorem span_mFourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p
     (span ℂ (range (@mFourierLp d _ p _))).topologicalClosure = ⊤ := by
   simpa only [map_span, ContinuousLinearMap.coe_coe, ← range_comp, Function.comp_def] using
     (ContinuousMap.toLp_denseRange ℂ volume ℂ hp).topologicalClosure_map_submodule
-      span_mFourier_closure_eq_top
+      (span_mFourier_closure_eq_top (d := d))
 
 /-- The monomials `mFourierLp 2 n` are an orthonormal set in `L²`. -/
 theorem orthonormal_mFourier : Orthonormal ℂ (mFourierLp (d := d) 2) := by
diff --git a/Mathlib/Analysis/InnerProductSpace/Defs.lean b/Mathlib/Analysis/InnerProductSpace/Defs.lean
index 78e3e893066037..8801e93d08857c 100644
--- a/Mathlib/Analysis/InnerProductSpace/Defs.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Defs.lean
@@ -510,7 +510,7 @@ lemma topology_eq
     tF = cd.toNormedAddCommGroup.toMetricSpace.toUniformSpace.toTopologicalSpace := by
   let p : Seminorm 𝕜 F := @normSeminorm 𝕜 F _ cd.toNormedAddCommGroup.toSeminormedAddCommGroup
     InnerProductSpace.Core.toNormedSpace
-  suffices WithSeminorms (fun (i : Fin 1) ↦ p) by
+  suffices WithSeminorms (fun (i : Unit) ↦ p) by
     rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 this]
     simp
   have : p.ball 0 1 = {v | re (cd.inner v v) < 1} := by
diff --git a/Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean b/Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean
index c359ff6784ae6c..36599b0148cd5f 100644
--- a/Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean
+++ b/Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean
@@ -63,7 +63,7 @@ theorem isInducing_inducingFn : Topology.IsInducing (inducingFn σ E F) :=
   (PointwiseConvergenceCLM.isEmbedding_coeFn σ E F).isInducing
 
 lemma withSeminorms : WithSeminorms (PointwiseConvergenceCLM.seminormFamily σ E F) :=
-  let e : E ≃ (Σ _ : E, Fin 1) := .symm <| .sigmaUnique _ _
+  let e : E ≃ (Σ _ : E, Unit) := .symm <| .sigmaUnique _ _
   (isInducing_inducingFn σ E F).withSeminorms <| withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜₂ F)
     |>.congr_equiv e
 
diff --git a/Mathlib/Analysis/LocallyConvex/WeakDual.lean b/Mathlib/Analysis/LocallyConvex/WeakDual.lean
index 881346ba1a82e5..f51e8b377a41af 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakDual.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakDual.lean
@@ -213,7 +213,7 @@ variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [M
 
 theorem LinearMap.weakBilin_withSeminorms (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
     WithSeminorms (LinearMap.toSeminormFamily B : F → Seminorm 𝕜 (WeakBilin B)) :=
-  let e : F ≃ (Σ _ : F, Fin 1) := .symm <| .sigmaUnique _ _
+  let e : F ≃ (Σ _ : F, Unit) := .symm <| .sigmaUnique _ _
   withSeminorms_induced (withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜 𝕜))
     (LinearMap.ltoFun 𝕜 F 𝕜 𝕜 ∘ₗ B : (WeakBilin B) →ₗ[𝕜] (F → 𝕜)) |>.congr_equiv e
 
diff --git a/Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean b/Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
index e97463ea879ff7..ad93b02d3f4e1e 100644
--- a/Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
+++ b/Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
@@ -406,7 +406,7 @@ def seminormFamily : SeminormFamily 𝕜₂ (E →SWOT[σ] F) (E × F⋆) :=
   fun ⟨x, y⟩ => seminorm x y
 
 lemma withSeminorms : WithSeminorms (seminormFamily σ E F) :=
-  let e : E × F⋆ ≃ (Σ _ : E × F⋆, Fin 1) := .symm <| .sigmaUnique _ _
+  let e : E × F⋆ ≃ (Σ _ : E × F⋆, Unit) := .symm <| .sigmaUnique _ _
   isInducing_inducingFn.withSeminorms <| withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜₂ 𝕜₂)
     |>.congr_equiv e
 
diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
index c213e5b124aba8..2e0516ecbde514 100644
--- a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
+++ b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
@@ -9,9 +9,10 @@ public import Mathlib.Analysis.LocallyConvex.Bounded
 public import Mathlib.Analysis.Normed.Module.Seminorm.Basic
 public import Mathlib.Analysis.Real.Sqrt
 public import Mathlib.Topology.Algebra.Equicontinuity
-public import Mathlib.Topology.MetricSpace.Equicontinuity
 public import Mathlib.Topology.Algebra.FilterBasis
+public import Mathlib.Topology.Algebra.Module.Equiv
 public import Mathlib.Topology.Algebra.Module.LocallyConvex
+public import Mathlib.Topology.MetricSpace.Equicontinuity
 
 /-!
 # Topology induced by a family of seminorms
@@ -24,6 +25,8 @@ public import Mathlib.Topology.Algebra.Module.LocallyConvex
   bounded by a finite number of seminorms in `E`.
 * `WithSeminorms p`, when `p` is a family of seminorms on `E`, is a proposition expressing that the
   (existing) topology on `E` is induced by the seminorms `p`.
+* `IsNormableSpace 𝕜 E` is a class asserting that the (existing) topology on `E` is induced
+  by *some* `𝕜`-seminorm
 * `PolynormableSpace 𝕜 E` is a class asserting that the (existing) topology on `E` is induced
   by *some* family of `𝕜`-seminorms. If `𝕜` is `RCLike`, this is equivalent to
   `LocallyConvexSpace 𝕜 E`.
@@ -59,7 +62,6 @@ seminorm, locally convex
 
 @[expose] public section
 
-
 open NormedField Set Seminorm TopologicalSpace Filter List Bornology
 
 open NNReal Pointwise Topology Uniformity
@@ -284,6 +286,18 @@ variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
 structure WithSeminorms (p : SeminormFamily 𝕜 E ι) [topology : TopologicalSpace E] : Prop where
   topology_eq_withSeminorms : topology = p.moduleFilterBasis.topology
 
+variable (𝕜 E) in
+/-- A topological vector space `E` is **normable** over `𝕜` if its topology is induced by
+*some* `𝕜`-seminorm. Note that this does not imply that the space is Hausdorff.
+To endow such a space with a normed space structure with the same topology, use:
+```
+  let : SeminormedAddCommGroup E := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E
+  let : NormedSpace 𝕜 E := IsNormableSpace.toNormedSpace 𝕜 E
+```
+-/
+class IsNormableSpace [topology : TopologicalSpace E] where
+  withSeminorms' : ∃ (p : Seminorm 𝕜 E), WithSeminorms (fun (_ : Unit) ↦ p)
+
 variable (𝕜 E) in
 /-- A topological vector space `E` is **polynormable** over `𝕜` if its topology is induced by
 *some* family of `𝕜`-seminorms. Equivalently, its topology is induced by *all* its continuous
@@ -313,6 +327,9 @@ theorem WithSeminorms.continuousSMul (hp : WithSeminorms p) : ContinuousSMul 
   rw [hp.withSeminorms_eq]
   exact ModuleFilterBasis.continuousSMul _
 
+instance [h : PolynormableSpace 𝕜 E] : ContinuousSMul 𝕜 E :=
+  h.withSeminorms'.continuousSMul
+
 theorem WithSeminorms.hasBasis (hp : WithSeminorms p) :
     (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basisSets) id := by
   rw [congr_fun (congr_arg (@nhds E) hp.1) 0]
@@ -474,6 +491,10 @@ theorem WithSeminorms.toPolynormableSpace {p : SeminormFamily 𝕜 E ι} (hp : W
       intro i
       exact iInf_le (ι := {p : Seminorm 𝕜 E // Continuous p}) _ ⟨p i, hp' i⟩
 
+instance [h : IsNormableSpace 𝕜 E] : PolynormableSpace 𝕜 E := by
+  rcases h.withSeminorms' with ⟨q, hq⟩
+  exact hq.toPolynormableSpace
+
 end TopologicalSpace
 
 /-- The uniform structure induced by a family of seminorms is exactly the infimum of the ones
@@ -494,14 +515,65 @@ section NormedSpace
 
 /-- The topology of a `NormedSpace 𝕜 E` is induced by the seminorm `normSeminorm 𝕜 E`. -/
 theorem norm_withSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
-    WithSeminorms fun _ : Fin 1 => normSeminorm 𝕜 E := by
+    WithSeminorms fun _ : Unit => normSeminorm 𝕜 E := by
   rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iInf_const, coe_normSeminorm,
     comap_norm_nhds_zero]
 
-/-- A (semi-)normed space is polynormable. -/
-instance [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
-    PolynormableSpace 𝕜 E :=
-  norm_withSeminorms 𝕜 E |>.toPolynormableSpace
+/-- A (semi-)normed space is normable. -/
+instance [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : IsNormableSpace 𝕜 E :=
+  ⟨⟨normSeminorm 𝕜 E, norm_withSeminorms 𝕜 E⟩⟩
+
+variable [NormedField 𝕜] [ha : AddCommGroup E] [hm : Module 𝕜 E]
+  [t : TopologicalSpace E] [hn : IsNormableSpace 𝕜 E]
+
+variable (𝕜 E)
+
+/-- A seminorm defining the topology in a normable space. -/
+noncomputable def IsNormableSpace.seminorm : Seminorm 𝕜 E := hn.withSeminorms'.choose
+
+/-- A normable space can be endowed with a seminorm defining the same topology. -/
+noncomputable abbrev IsNormableSpace.toSeminormedAddCommGroup : SeminormedAddCommGroup E := by
+  let q := IsNormableSpace.seminorm 𝕜 E
+  have hq := hn.withSeminorms'.choose_spec
+  have : IsTopologicalAddGroup E := hq.topologicalAddGroup
+  let : Norm E := ⟨IsNormableSpace.seminorm 𝕜 E⟩
+  let c : SeminormedSpace.Core 𝕜 E :=
+  { norm_nonneg x := apply_nonneg q x
+    norm_smul c x := map_smul_eq_mul q c x
+    norm_triangle x y := map_add_le_add q x y }
+  refine SeminormedAddCommGroup.ofCoreReplaceTopology c ?_
+  rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 hq, ciInf_unique]
+  rfl
+
+/-- A normable space can be endowed with a normed space structure. -/
+noncomputable abbrev IsNormableSpace.toNormedSpace :
+    letI : SeminormedAddCommGroup E := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E
+    NormedSpace 𝕜 E :=
+  letI : SeminormedAddCommGroup E := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E
+  { norm_smul_le c x := (map_smul_eq_mul (IsNormableSpace.seminorm 𝕜 E) c x).le }
+
+instance [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsNormableSpace 𝕜 F] :
+    IsNormableSpace 𝕜 (E × F) := by
+  let : SeminormedAddCommGroup E := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E
+  let : NormedSpace 𝕜 E := IsNormableSpace.toNormedSpace 𝕜 E
+  let : SeminormedAddCommGroup F := IsNormableSpace.toSeminormedAddCommGroup 𝕜 F
+  let : NormedSpace 𝕜 F := IsNormableSpace.toNormedSpace 𝕜 F
+  infer_instance
+
+instance {E : ι → Type*} [Finite ι] [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
+    [∀ i, TopologicalSpace (E i)] [∀ i, IsNormableSpace 𝕜 (E i)] :
+    IsNormableSpace 𝕜 (Π i, E i) := by
+  let A i : SeminormedAddCommGroup (E i) := IsNormableSpace.toSeminormedAddCommGroup 𝕜 (E i)
+  let B i : NormedSpace 𝕜 (E i) := IsNormableSpace.toNormedSpace 𝕜 (E i)
+  let : Fintype ι := Fintype.ofFinite ι
+  infer_instance
+
+include 𝕜 in
+/-- A normable space is metrizable. Not an instance as the field of scalars can not be guessed
+by typeclass inference. -/
+theorem IsNormableSpace.toPseudoMetrizableSpace : PseudoMetrizableSpace E := by
+  let : SeminormedAddCommGroup E := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E
+  infer_instance
 
 end NormedSpace
 
@@ -581,7 +653,7 @@ theorem WithSeminorms.isVonNBounded_iff_seminorm_bddAbove {s : Set E} (hp : With
 the unit ball for this seminorm is a bounded neighborhood of `0`. -/
 theorem withSeminorms_iff_mem_nhds_isVonNBounded [IsTopologicalAddGroup E]
     [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} :
-    WithSeminorms (fun (_ : Fin 1) ↦ p) ↔ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1) := by
+    WithSeminorms (fun (_ : Unit) ↦ p) ↔ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1) := by
   /- The nontrivial direction is from right to left. With `SeminormFamily.withSeminorms_of_nhds`,
   we need to see that the neighborhoods of zero for the initial topology and for `p` coincide. -/
   refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
@@ -604,7 +676,7 @@ theorem withSeminorms_iff_mem_nhds_isVonNBounded [IsTopologicalAddGroup E]
       rwa [smul_set_subset_smul_set_iff₀ c_ne] at this
     grw [← this]
     apply FilterBasis.mem_filter_of_mem
-    change p.ball 0 (‖c⁻¹‖) ∈ SeminormFamily.basisSets (fun (i : Fin 1) ↦ p)
+    change p.ball 0 (‖c⁻¹‖) ∈ SeminormFamily.basisSets (fun (i : Unit) ↦ p)
     apply SeminormFamily.basisSets_singleton_mem _ 0
     simpa using c_ne
   · /- Show that a neighborhood `s` for `p` is a neighborhood for the topology, by using the
@@ -685,7 +757,7 @@ theorem continuous_normedSpace_rng (F) [SeminormedAddCommGroup F] [NormedSpace 
     [TopologicalSpace E] {p : ι → Seminorm 𝕝 E} (hp : WithSeminorms p)
     (f : E →ₛₗ[τ₁₂] F) (hf : ∃ (s : Finset ι) (C : ℝ≥0), (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) :
     Continuous f := by
-  rw [← Seminorm.isBounded_const (Fin 1)] at hf
+  rw [← Seminorm.isBounded_const Unit] at hf
   exact continuous_of_isBounded hp (norm_withSeminorms 𝕝₂ F) f hf
 
 lemma _root_.Seminorm.abs_le_of_le [Module ℝ E] {p : Seminorm ℝ E}
@@ -707,7 +779,7 @@ theorem continuous_normedSpace_dom (E) [SeminormedAddCommGroup E] [NormedSpace 
     [TopologicalSpace F] {q : ι → Seminorm 𝕝₂ F} (hq : WithSeminorms q)
     (f : E →ₛₗ[τ₁₂] F) (hf : ∀ i : ι, ∃ C : ℝ≥0, (q i).comp f ≤ C • normSeminorm 𝕝 E) :
     Continuous f := by
-  rw [← Seminorm.const_isBounded (Fin 1)] at hf
+  rw [← Seminorm.const_isBounded Unit] at hf
   exact continuous_of_isBounded (norm_withSeminorms 𝕝 E) hq f hf
 
 @[deprecated (since := "2026-03-09")]
@@ -1008,15 +1080,37 @@ lemma Topology.IsInducing.withSeminorms {q : SeminormFamily 𝕜₂ F ι}
   rw [hf.eq_induced]
   exact f.withSeminorms_induced hq
 
+theorem Topology.IsInducing.isNormableSpace [h : IsNormableSpace 𝕜₂ F]
+    [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing f) :
+    IsNormableSpace 𝕜 E := by
+  rcases h.withSeminorms' with ⟨p, hp⟩
+  exact ⟨p.comp f, hf.withSeminorms hp⟩
+
 theorem Topology.IsInducing.polynormableSpace [PolynormableSpace 𝕜₂ F]
     [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing f) :
     PolynormableSpace 𝕜 E :=
   hf.withSeminorms (PolynormableSpace.withSeminorms 𝕜₂ F) |>.toPolynormableSpace
 
+instance [IsNormableSpace 𝕜₂ F] {S : Submodule 𝕜₂ F} :
+    IsNormableSpace 𝕜₂ S :=
+  IsInducing.isNormableSpace (f := S.subtype) .subtypeVal
+
 instance [PolynormableSpace 𝕜₂ F] {S : Submodule 𝕜₂ F} :
     PolynormableSpace 𝕜₂ S :=
   IsInducing.polynormableSpace (f := S.subtype) .subtypeVal
 
+theorem ContinuousLinearEquiv.isNormableSpace {σ₂₁ : 𝕜₂ →+* 𝕜}
+    [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [IsNormableSpace 𝕜₂ F]
+    [TopologicalSpace E] (f : E ≃SL[σ₁₂] F) :
+    IsNormableSpace 𝕜 E :=
+  f.toHomeomorph.isInducing.isNormableSpace
+
+theorem ContinuousLinearEquiv.PolynormableSpace {σ₂₁ : 𝕜₂ →+* 𝕜}
+    [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [PolynormableSpace 𝕜₂ F]
+    [TopologicalSpace E] (f : E ≃SL[σ₁₂] F) :
+    PolynormableSpace 𝕜 E :=
+  f.toHomeomorph.isInducing.polynormableSpace
+
 section NontriviallyNormedField
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [Module 𝕜 E] [TopologicalSpace E]
diff --git a/Mathlib/Analysis/Normed/Module/Dual.lean b/Mathlib/Analysis/Normed/Module/Dual.lean
index 84194fdb1f8027..caa677e04a13c8 100644
--- a/Mathlib/Analysis/Normed/Module/Dual.lean
+++ b/Mathlib/Analysis/Normed/Module/Dual.lean
@@ -59,7 +59,7 @@ theorem polar_closure (s : Set E) : StrongDual.polar 𝕜 (closure s) = StrongDu
     (topDualPairing 𝕜 E).flip.polar_gc.l_le <|
       closure_minimal ((topDualPairing 𝕜 E).flip.polar_gc.le_u_l s) <| by
         simpa [LinearMap.flip_flip] using!
-          (isClosed_polar _ _).preimage (ContinuousLinearMap.apply 𝕜 𝕜 (E := E)).continuous
+          (isClosed_polar _ _).preimage (ContinuousLinearMap.apply 𝕜 𝕜 (E' := E)).continuous
 
 variable {𝕜}
 
diff --git a/Mathlib/Analysis/Normed/Operator/Basic.lean b/Mathlib/Analysis/Normed/Operator/Basic.lean
index 2ed7ced28524d5..b8463fb2d18044 100644
--- a/Mathlib/Analysis/Normed/Operator/Basic.lean
+++ b/Mathlib/Analysis/Normed/Operator/Basic.lean
@@ -389,6 +389,16 @@ instance toNormedSpace {𝕜' : Type*} [NormedField 𝕜'] [NormedSpace 𝕜' F]
     NormedSpace 𝕜' (E →SL[σ₁₂] F) :=
   ⟨opNorm_smul_le⟩
 
+instance {E F : Type*} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsNormableSpace 𝕜 E]
+    [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [IsTopologicalAddGroup F]
+    [IsNormableSpace 𝕜₂ F] :
+    IsNormableSpace 𝕜₂ (E →SL[σ₁₂] F) := by
+  let : SeminormedAddCommGroup E := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E
+  let : NormedSpace 𝕜 E := IsNormableSpace.toNormedSpace 𝕜 E
+  let : SeminormedAddCommGroup F := IsNormableSpace.toSeminormedAddCommGroup 𝕜₂ F
+  let : NormedSpace 𝕜₂ F := IsNormableSpace.toNormedSpace 𝕜₂ F
+  infer_instance
+
 /-- The operator norm is submultiplicative. -/
 theorem opNorm_comp_le (f : E →SL[σ₁₂] F) : ‖h.comp f‖ ≤ ‖h‖ * ‖f‖ :=
   csInf_le bounds_bddBelow ⟨by positivity, fun x => by
diff --git a/Mathlib/Analysis/Normed/Operator/Bilinear.lean b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
index cc464034a7b100..b91074f63b70f3 100644
--- a/Mathlib/Analysis/Normed/Operator/Bilinear.lean
+++ b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
@@ -25,7 +25,7 @@ open Filter hiding map_smul
 open scoped NNReal Topology Uniformity
 
 -- the `ₗ` subscript variables are for special cases about linear (as opposed to semilinear) maps
-variable {𝕜 𝕜₂ 𝕜₃ E Eₗ F Fₗ G Gₗ : Type*}
+variable {𝕜 𝕜₂ 𝕜₃ E Eₗ E' Eₗ' F Fₗ F' Fₗ' G Gₗ G' Gₗ' : Type*}
 
 section SemiNormed
 
@@ -39,6 +39,14 @@ variable [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [Nontr
   [NormedSpace 𝕜 Gₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
   [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
 
+variable
+  [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E']
+  [AddCommGroup Eₗ'] [Module 𝕜 Eₗ'] [TopologicalSpace Eₗ'] [IsNormableSpace 𝕜 Eₗ']
+  [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F']
+  [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ']
+  [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G']
+  [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ']
+
 namespace ContinuousLinearMap
 
 section OpNorm
@@ -134,21 +142,61 @@ theorem mkContinuous₂_norm_le (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃]
     (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) : ‖f.mkContinuous₂ C hC‖ ≤ C :=
   (f.mkContinuous₂_norm_le' hC).trans_eq <| max_eq_left h0
 
+/-- Given a bilinear map, convert it to a continuous bilinear map if there exists a continuous
+bilinear map which coincides with it.
+This may seem silly: why not use the witness directly? The reason to use this is good
+definitional behavior: in use cases for normable spaces, the witness is constructed by putting a
+norm on the space, so it has a complicated definition which the kernel struggles with, while
+the output of the current definition is definitionally much nicer.
+-/
+def mkContinuous₂OfExists [IsTopologicalAddGroup G'] (f : E' →ₛₗ[σ₁₃] F' →ₛₗ[σ₂₃] G')
+    (hf : ∃ g : E' →SL[σ₁₃] F' →SL[σ₂₃] G', ∀ a b, f a b = g a b) :
+    E' →SL[σ₁₃] F' →SL[σ₂₃] G' where
+  toFun a :=
+    { toFun b := f a b
+      map_add' b b' := by simp
+      map_smul' c b := by simp
+      cont := by
+        rcases hf with ⟨g, hg⟩
+        convert (g a).continuous
+        apply hg }
+  map_add' a a' := by ext; simp
+  map_smul' c a := by ext; simp
+  cont := by
+    rcases hf with ⟨g, hg⟩
+    convert g.continuous
+    apply hg
+
 end LinearMap
 
 namespace ContinuousLinearMap
 
 variable [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃]
+  [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] [IsTopologicalAddGroup Gₗ']
+
+/-- Flip the order of arguments of a continuous bilinear map. Linear version.
+Do not use: use instead `flip` which outputs a continuous bilinear map. -/
+def flipₗ (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : F' →ₛₗ[σ₂₃] E' →ₛₗ[σ₁₃] G' :=
+  LinearMap.mk₂'ₛₗ σ₂₃ σ₁₃ (fun y x => f x y) (fun x y z => (f z).map_add x y)
+      (fun c y x => (f x).map_smulₛₗ c y) (fun z x y => by simp only [f.map_add, add_apply])
+        (fun c y x => by simp only [f.map_smulₛₗ, smul_apply])
+
+lemma exists_eq_flipₗ (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') :
+    ∃ g : F' →SL[σ₂₃] E' →SL[σ₁₃] G', ∀ a b, flipₗ f a b = g a b := by
+  let : SeminormedAddCommGroup E' := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E'
+  let : NormedSpace 𝕜 E' := IsNormableSpace.toNormedSpace 𝕜 E'
+  let : SeminormedAddCommGroup F' := IsNormableSpace.toSeminormedAddCommGroup 𝕜₂ F'
+  let : NormedSpace 𝕜₂ F' := IsNormableSpace.toNormedSpace 𝕜₂ F'
+  let : SeminormedAddCommGroup G' := IsNormableSpace.toSeminormedAddCommGroup 𝕜₃ G'
+  let : NormedSpace 𝕜₃ G' := IsNormableSpace.toNormedSpace 𝕜₃ G'
+  exact ⟨LinearMap.mkContinuous₂ (flipₗ f)
+    ‖f‖ fun y x => (f.le_opNorm₂ x y).trans_eq <| by simp only [mul_right_comm], fun a b ↦ rfl⟩
 
 /-- Flip the order of arguments of a continuous bilinear map.
 For a version bundled as `LinearIsometryEquiv`, see
 `ContinuousLinearMap.flipL`. -/
-def flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : F →SL[σ₂₃] E →SL[σ₁₃] G :=
-  LinearMap.mkContinuous₂
-    (LinearMap.mk₂'ₛₗ σ₂₃ σ₁₃ (fun y x => f x y) (fun x y z => (f z).map_add x y)
-      (fun c y x => (f x).map_smulₛₗ c y) (fun z x y => by simp only [f.map_add, add_apply])
-        (fun c y x => by simp only [f.map_smulₛₗ, smul_apply]))
-    ‖f‖ fun y x => (f.le_opNorm₂ x y).trans_eq <| by simp only [mul_right_comm]
+def flip (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : F' →SL[σ₂₃] E' →SL[σ₁₃] G' :=
+  (flipₗ f).mkContinuous₂OfExists (exists_eq_flipₗ f)
 
 private theorem le_norm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f‖ ≤ ‖flip f‖ :=
   f.opNorm_le_bound₂ (norm_nonneg f.flip) fun x y => by
@@ -156,11 +204,11 @@ private theorem le_norm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f
     exact (flip f).le_opNorm₂ y x
 
 @[simp]
-theorem flip_apply (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) : f.flip y x = f x y :=
+theorem flip_apply (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') (x : E') (y : F') : f.flip y x = f x y :=
   rfl
 
 @[simp]
-theorem flip_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : f.flip.flip = f := by
+theorem flip_flip (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : f.flip.flip = f := by
   ext
   rfl
 
@@ -177,14 +225,14 @@ theorem opENorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖
   simp [enorm_eq_nnnorm]
 
 @[simp]
-lemma flip_zero : flip (0 : E →SL[σ₁₃] F →SL[σ₂₃] G) = 0 := rfl
+lemma flip_zero : flip (0 : E' →SL[σ₁₃] F' →SL[σ₂₃] G') = 0 := rfl
 
 @[simp]
-theorem flip_add (f g : E →SL[σ₁₃] F →SL[σ₂₃] G) : (f + g).flip = f.flip + g.flip :=
+theorem flip_add (f g : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : (f + g).flip = f.flip + g.flip :=
   rfl
 
 @[simp]
-theorem flip_smul (c : 𝕜₃) (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : (c • f).flip = c • f.flip :=
+theorem flip_smul (c : 𝕜₃) (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : (c • f).flip = c • f.flip :=
   rfl
 
 variable (E F G σ₁₃ σ₂₃)
@@ -235,95 +283,111 @@ theorem flipₗᵢ_symm : (flipₗᵢ 𝕜 E Fₗ Gₗ).symm = flipₗᵢ 𝕜 F
 theorem coe_flipₗᵢ : ⇑(flipₗᵢ 𝕜 E Fₗ Gₗ) = flip :=
   rfl
 
-variable (F σ₁₂)
-variable [RingHomIsometric σ₁₂]
+variable (F' σ₁₂)
+variable [RingHomIsometric σ₁₂] [IsTopologicalAddGroup F'] [IsTopologicalAddGroup Fₗ']
 
 /-- The continuous semilinear map obtained by applying a continuous semilinear map at a given
 vector.
 
 This is the continuous version of `LinearMap.applyₗ`. -/
-def apply' : E →SL[σ₁₂] (E →SL[σ₁₂] F) →L[𝕜₂] F :=
-  flip (.id 𝕜₂ (E →SL[σ₁₂] F))
+def apply' : E' →SL[σ₁₂] (E' →SL[σ₁₂] F') →L[𝕜₂] F' :=
+  flip (.id 𝕜₂ (E' →SL[σ₁₂] F'))
 
-variable {F σ₁₂}
+variable {F' σ₁₂}
 
 @[simp]
-theorem apply_apply' (v : E) (f : E →SL[σ₁₂] F) : apply' F σ₁₂ v f = f v :=
+theorem apply_apply' (v : E') (f : E' →SL[σ₁₂] F') : apply' F' σ₁₂ v f = f v :=
   rfl
 
-variable (𝕜 Fₗ)
+variable (𝕜 Fₗ')
 
 /-- The continuous semilinear map obtained by applying a continuous semilinear map at a given
 vector.
 
 This is the continuous version of `LinearMap.applyₗ`. -/
-def apply : E →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] Fₗ :=
-  flip (.id 𝕜 (E →L[𝕜] Fₗ))
+def apply : E' →L[𝕜] (E' →L[𝕜] Fₗ') →L[𝕜] Fₗ' :=
+  flip (.id 𝕜 (E' →L[𝕜] Fₗ'))
 
-variable {𝕜 Fₗ}
+variable {𝕜 Fₗ'}
 
 @[simp]
-theorem apply_apply (v : E) (f : E →L[𝕜] Fₗ) : apply 𝕜 Fₗ v f = f v :=
+theorem apply_apply (v : E') (f : E' →L[𝕜] Fₗ') : apply 𝕜 Fₗ' v f = f v :=
   rfl
 
-variable (σ₁₂ σ₂₃ E F G)
-
+variable (σ₁₂ σ₂₃ E F G E' F' G')
+
+/-- Composition of continuous semilinear maps as a semibilinear map.
+Do not use: use instead the version `compSL` which outputs a continuous semibilinear map. -/
+def compSLₗ : (F' →SL[σ₂₃] G') →ₗ[𝕜₃] (E' →SL[σ₁₂] F') →ₛₗ[σ₂₃] E' →SL[σ₁₃] G' :=
+  LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ comp add_comp smul_comp comp_add
+    fun c f g => by ext; simp only [map_smulₛₗ, comp_apply, smul_apply]
+
+lemma exists_eq_compSLₗ :
+    ∃ g : (F' →SL[σ₂₃] G') →L[𝕜₃] (E' →SL[σ₁₂] F') →SL[σ₂₃] E' →SL[σ₁₃] G',
+      ∀ a b, compSLₗ E' F' G' σ₁₂ σ₂₃ a b = g a b := by
+  let : SeminormedAddCommGroup E' := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E'
+  let : NormedSpace 𝕜 E' := IsNormableSpace.toNormedSpace 𝕜 E'
+  let : SeminormedAddCommGroup F' := IsNormableSpace.toSeminormedAddCommGroup 𝕜₂ F'
+  let : NormedSpace 𝕜₂ F' := IsNormableSpace.toNormedSpace 𝕜₂ F'
+  let : SeminormedAddCommGroup G' := IsNormableSpace.toSeminormedAddCommGroup 𝕜₃ G'
+  let : NormedSpace 𝕜₃ G' := IsNormableSpace.toNormedSpace 𝕜₃ G'
+  exact ⟨LinearMap.mkContinuous₂ (compSLₗ E' F' G' σ₁₂ σ₂₃) 1
+    fun f g => by simpa only [one_mul] using! opNorm_comp_le f g, fun a b ↦ rfl⟩
 
 /-- Composition of continuous semilinear maps as a continuous semibilinear map. -/
-def compSL : (F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G :=
-  LinearMap.mkContinuous₂
-    (LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ comp add_comp smul_comp comp_add fun c f g => by
-      ext
-      simp only [map_smulₛₗ, comp_apply, smul_apply])
-    1 fun f g => by simpa only [one_mul] using! opNorm_comp_le f g
+def compSL : (F' →SL[σ₂₃] G') →L[𝕜₃] (E' →SL[σ₁₂] F') →SL[σ₂₃] E' →SL[σ₁₃] G' :=
+  (compSLₗ E' F' G' σ₁₂ σ₂₃).mkContinuous₂OfExists (exists_eq_compSLₗ E' F' G' σ₁₂ σ₂₃)
 
 theorem norm_compSL_le : ‖compSL E F G σ₁₂ σ₂₃‖ ≤ 1 :=
-  LinearMap.mkContinuous₂_norm_le _ zero_le_one _
+  ContinuousLinearMap.opNorm_le_bound₂ _ zero_le_one
+    fun f g => by simpa only [one_mul] using! opNorm_comp_le f g
 
-variable {σ₁₂ σ₂₃ E F G}
+variable {σ₁₂ σ₂₃ E F G E' F' G'}
 
 @[simp]
-theorem compSL_apply (f : F →SL[σ₂₃] G) (g : E →SL[σ₁₂] F) : compSL E F G σ₁₂ σ₂₃ f g = f.comp g :=
+theorem compSL_apply (f : F' →SL[σ₂₃] G') (g : E' →SL[σ₁₂] F') :
+    compSL E' F' G' σ₁₂ σ₂₃ f g = f.comp g :=
   rfl
 
-theorem _root_.Continuous.const_clm_comp {X} [TopologicalSpace X] {f : X → E →SL[σ₁₂] F}
-    (hf : Continuous f) (g : F →SL[σ₂₃] G) :
-    Continuous (fun x => g.comp (f x) : X → E →SL[σ₁₃] G) :=
-  (compSL E F G σ₁₂ σ₂₃ g).continuous.comp hf
+theorem _root_.Continuous.const_clm_comp {X} [TopologicalSpace X] {f : X → E' →SL[σ₁₂] F'}
+    (hf : Continuous f) (g : F' →SL[σ₂₃] G') :
+    Continuous (fun x => g.comp (f x) : X → E' →SL[σ₁₃] G') :=
+  (compSL E' F' G' σ₁₂ σ₂₃ g).continuous.comp hf
 
--- Giving the implicit argument speeds up elaboration significantly
-theorem _root_.Continuous.clm_comp_const {X} [TopologicalSpace X] {g : X → F →SL[σ₂₃] G}
-    (hg : Continuous g) (f : E →SL[σ₁₂] F) :
-    Continuous (fun x => (g x).comp f : X → E →SL[σ₁₃] G) :=
-  (@ContinuousLinearMap.flip _ _ _ _ _ (E →SL[σ₁₃] G) _ _ _ _ _ _ _ _ _ _ _ _ _
-    (compSL E F G σ₁₂ σ₂₃) f).continuous.comp hg
+theorem _root_.Continuous.clm_comp_const {X} [TopologicalSpace X] {g : X → F' →SL[σ₂₃] G'}
+    (hg : Continuous g) (f : E' →SL[σ₁₂] F') :
+    Continuous (fun x => (g x).comp f : X → E' →SL[σ₁₃] G') :=
+  (ContinuousLinearMap.flip (compSL E' F' G' σ₁₂ σ₂₃) f).continuous.comp hg
 
-variable (𝕜 σ₁₂ σ₂₃ E Fₗ Gₗ)
+variable (𝕜 σ₁₂ σ₂₃ E E' Fₗ Fₗ' Gₗ Gₗ')
 
 /-- Composition of continuous linear maps as a continuous bilinear map. -/
-def compL : (Fₗ →L[𝕜] Gₗ) →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] Gₗ :=
-  compSL E Fₗ Gₗ (RingHom.id 𝕜) (RingHom.id 𝕜)
+def compL : (Fₗ' →L[𝕜] Gₗ') →L[𝕜] (E' →L[𝕜] Fₗ') →L[𝕜] E' →L[𝕜] Gₗ' :=
+  compSL E' Fₗ' Gₗ' (RingHom.id 𝕜) (RingHom.id 𝕜)
 
 theorem norm_compL_le : ‖compL 𝕜 E Fₗ Gₗ‖ ≤ 1 :=
   norm_compSL_le _ _ _ _ _
 
 @[simp]
-theorem compL_apply (f : Fₗ →L[𝕜] Gₗ) (g : E →L[𝕜] Fₗ) : compL 𝕜 E Fₗ Gₗ f g = f.comp g :=
+theorem compL_apply (f : Fₗ' →L[𝕜] Gₗ') (g : E' →L[𝕜] Fₗ') : compL 𝕜 E' Fₗ' Gₗ' f g = f.comp g :=
   rfl
 
-variable (Eₗ) {𝕜 E Fₗ Gₗ}
+variable (Eₗ Eₗ') {𝕜 E E' Fₗ Fₗ' Gₗ Gₗ'}
 
 /-- Apply `L(x,-)` pointwise to bilinear maps, as a continuous bilinear map -/
 @[simps! apply]
-def precompR (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : E →L[𝕜] (Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ :=
-  compL 𝕜 Eₗ Fₗ Gₗ ∘L L
+def precompR (L : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') : E' →L[𝕜] (Eₗ' →L[𝕜] Fₗ') →L[𝕜] Eₗ' →L[𝕜] Gₗ' :=
+  compL 𝕜 Eₗ' Fₗ' Gₗ' ∘L L
+
+variable [IsTopologicalAddGroup E']
 
 /-- Apply `L(-,y)` pointwise to bilinear maps, as a continuous bilinear map -/
-def precompL (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : (Eₗ →L[𝕜] E) →L[𝕜] Fₗ →L[𝕜] Eₗ →L[𝕜] Gₗ :=
-  (precompR Eₗ (flip L)).flip
+def precompL (L : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') : (Eₗ' →L[𝕜] E') →L[𝕜] Fₗ' →L[𝕜] Eₗ' →L[𝕜] Gₗ' :=
+  (precompR Eₗ' (flip L)).flip
 
-@[simp] lemma precompL_apply (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (u : Eₗ →L[𝕜] E) (f : Fₗ) (g : Eₗ) :
-    precompL Eₗ L u f g = L (u g) f := rfl
+omit [IsTopologicalAddGroup Fₗ'] in
+@[simp] lemma precompL_apply (L : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') (u : Eₗ' →L[𝕜] E') (f : Fₗ') (g : Eₗ') :
+    precompL Eₗ' L u f g = L (u g) f := rfl
 
 theorem norm_precompR_le (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : ‖precompR Eₗ L‖ ≤ ‖L‖ :=
   calc
@@ -339,48 +403,52 @@ end ContinuousLinearMap
 
 namespace ContinuousLinearMap
 
-variable {E' F' : Type*} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F']
+variable {E'' F'' : Type*} [AddCommGroup E''] [AddCommGroup F'']
+  [TopologicalSpace E''] [TopologicalSpace F'']
+  [IsTopologicalAddGroup G'] [IsTopologicalAddGroup Gₗ']
 variable {𝕜₁' : Type*} {𝕜₂' : Type*} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂']
-  [NormedSpace 𝕜₁' E'] [NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}
+  [Module 𝕜₁' E''] [Module 𝕜₂' F''] [IsNormableSpace 𝕜₁' E''] [IsNormableSpace 𝕜₂' F'']
+  {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}
   {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃']
   [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃']
 
-/-- Compose a bilinear map `E →SL[σ₁₃] F →SL[σ₂₃] G` with two linear maps
-`E' →SL[σ₁'] E` and `F' →SL[σ₂'] F`. -/
-def bilinearComp (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (gE : E' →SL[σ₁'] E) (gF : F' →SL[σ₂'] F) :
-    E' →SL[σ₁₃'] F' →SL[σ₂₃'] G :=
+/-- Compose a bilinear map `E' →SL[σ₁₃] F' →SL[σ₂₃] G'` with two linear maps
+`E'' →SL[σ₁'] E'` and `F'' →SL[σ₂'] F'`. -/
+def bilinearComp (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') (gE : E'' →SL[σ₁'] E') (gF : F'' →SL[σ₂'] F') :
+    E'' →SL[σ₁₃'] F'' →SL[σ₂₃'] G' :=
   ((f.comp gE).flip.comp gF).flip
 
 @[simp]
-theorem bilinearComp_apply (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (gE : E' →SL[σ₁'] E) (gF : F' →SL[σ₂'] F)
-    (x : E') (y : F') : f.bilinearComp gE gF x y = f (gE x) (gF y) :=
+theorem bilinearComp_apply
+    (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') (gE : E'' →SL[σ₁'] E') (gF : F'' →SL[σ₂'] F')
+    (x : E'') (y : F'') : f.bilinearComp gE gF x y = f (gE x) (gF y) :=
   rfl
 
 @[simp]
-lemma bilinearComp_zero {gE : E' →SL[σ₁'] E} {gF : F' →SL[σ₂'] F} :
-    bilinearComp (0 : E →SL[σ₁₃] F →SL[σ₂₃] G) gE gF = 0 := rfl
+lemma bilinearComp_zero {gE : E'' →SL[σ₁'] E'} {gF : F'' →SL[σ₂'] F'} :
+    bilinearComp (0 : E' →SL[σ₁₃] F' →SL[σ₂₃] G') gE gF = 0 := rfl
 
 @[simp]
-lemma bilinearComp_zero_left {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gF : F' →SL[σ₂'] F} :
-    bilinearComp f (0 : E' →SL[σ₁'] E) gF = 0 := by ext; simp
+lemma bilinearComp_zero_left {f : E' →SL[σ₁₃] F' →SL[σ₂₃] G'} {gF : F'' →SL[σ₂'] F'} :
+    bilinearComp f (0 : E'' →SL[σ₁'] E') gF = 0 := by ext; simp
 
 @[simp]
-lemma bilinearComp_zero_right {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gE : E' →SL[σ₁'] E} :
-    bilinearComp f gE (0 : F' →SL[σ₂'] F) = 0 := by ext; simp
+lemma bilinearComp_zero_right {f : E' →SL[σ₁₃] F' →SL[σ₂₃] G'} {gE : E'' →SL[σ₁'] E'} :
+    bilinearComp f gE (0 : F'' →SL[σ₂'] F') = 0 := by ext; simp
 
-variable [RingHomIsometric σ₁₃] [RingHomIsometric σ₁'] [RingHomIsometric σ₂']
+variable [RingHomIsometric σ₁₃] [RingHomIsometric σ₁'] [RingHomIsometric σ₂'] [IsNormableSpace 𝕜 E']
 
 /-- Derivative of a continuous bilinear map `f : E →L[𝕜] F →L[𝕜] G` interpreted as a map `E × F → G`
 at point `p : E × F` evaluated at `q : E × F`, as a continuous bilinear map. -/
-def deriv₂ (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : E × Fₗ →L[𝕜] E × Fₗ →L[𝕜] Gₗ :=
+def deriv₂ (f : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') : E' × Fₗ' →L[𝕜] E' × Fₗ' →L[𝕜] Gₗ' :=
   f.bilinearComp (fst _ _ _) (snd _ _ _) + f.flip.bilinearComp (snd _ _ _) (fst _ _ _)
 
 @[simp]
-theorem coe_deriv₂ (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (p : E × Fₗ) :
-    ⇑(f.deriv₂ p) = fun q : E × Fₗ => f p.1 q.2 + f q.1 p.2 :=
+theorem coe_deriv₂ (f : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') (p : E' × Fₗ') :
+    ⇑(f.deriv₂ p) = fun q : E' × Fₗ' => f p.1 q.2 + f q.1 p.2 :=
   rfl
 
-theorem map_add_add (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (x x' : E) (y y' : Fₗ) :
+theorem map_add_add (f : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') (x x' : E') (y y' : Fₗ') :
     f (x + x') (y + y') = f x y + f.deriv₂ (x, y) (x', y') + f x' y' := by
   simp only [map_add, add_apply, coe_deriv₂, add_assoc]
   abel
@@ -417,25 +485,41 @@ theorem nnnorm_smulRight_apply (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRight
 @[simp] theorem nnnorm_toSpanSingleton (x : E) : ‖toSpanSingleton 𝕜 x‖₊ = ‖x‖₊ :=
   NNReal.eq <| norm_toSpanSingleton _
 
-variable (𝕜 E Fₗ) in
+variable [IsTopologicalAddGroup Fₗ']
+variable (𝕜 E' Fₗ')
+
+/-- `ContinuousLinearMap.smulRight` as a trilinear map:
+`smulRightLₗ (c : StrongDual 𝕜 E) (f : F) (x : E) = c x • f`.
+Do not use: use instead `smulRightL` which outputs a continuous trilinear map. -/
+@[simps! apply_apply]
+def smulRightLₗ : StrongDual 𝕜 E' →ₗ[𝕜] Fₗ' →ₗ[𝕜] E' →L[𝕜] Fₗ' where
+  toFun := smulRightₗ
+  map_add' := fun c₁ c₂ => by
+    ext x
+    simp only [add_smul, coe_smulRightₗ, add_apply, smulRight_apply, LinearMap.add_apply]
+  map_smul' := fun m c => by
+    ext x
+    simp [smul_smul]
+
+lemma exists_eq_smulRightLₗ :
+    ∃ g : StrongDual 𝕜 E' →L[𝕜] Fₗ' →L[𝕜] E' →L[𝕜] Fₗ',
+      ∀ a b, smulRightLₗ 𝕜 E' Fₗ' a b = g a b := by
+  let : SeminormedAddCommGroup E' := IsNormableSpace.toSeminormedAddCommGroup 𝕜 E'
+  let : NormedSpace 𝕜 E' := IsNormableSpace.toNormedSpace 𝕜 E'
+  let : SeminormedAddCommGroup Fₗ' := IsNormableSpace.toSeminormedAddCommGroup 𝕜 Fₗ'
+  let : NormedSpace 𝕜 Fₗ' := IsNormableSpace.toNormedSpace 𝕜 Fₗ'
+  exact ⟨LinearMap.mkContinuous₂ (smulRightLₗ 𝕜 E' Fₗ') 1
+    fun c x => by simp only [smulRightLₗ, coe_smulRightₗ, one_mul, norm_smulRight_apply,
+      LinearMap.coe_mk, AddHom.coe_mk, le_refl], fun a b ↦ rfl⟩
+
 /-- `ContinuousLinearMap.smulRight` as a continuous trilinear map:
 `smulRightL (c : StrongDual 𝕜 E) (f : F) (x : E) = c x • f`.
 
 This is also known as a rank-one operator.
 See also `InnerProductSpace.rankOne` for the rank-one operator on Hilbert spaces. -/
 @[simps! apply_apply]
-def smulRightL : StrongDual 𝕜 E →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ :=
-  LinearMap.mkContinuous₂
-    { toFun := smulRightₗ
-      map_add' := fun c₁ c₂ => by
-        ext x
-        simp only [add_smul, coe_smulRightₗ, add_apply, smulRight_apply, LinearMap.add_apply]
-      map_smul' := fun m c => by
-        ext x
-        simp [smul_smul] }
-    1 fun c x => by
-      simp only [coe_smulRightₗ, one_mul, norm_smulRight_apply, LinearMap.coe_mk, AddHom.coe_mk,
-        le_refl]
+def smulRightL : StrongDual 𝕜 E' →L[𝕜] Fₗ' →L[𝕜] E' →L[𝕜] Fₗ' :=
+  (smulRightLₗ 𝕜 E' Fₗ').mkContinuous₂OfExists (exists_eq_smulRightLₗ 𝕜 E' Fₗ')
 
 end ContinuousLinearMap
 
diff --git a/Mathlib/Analysis/Normed/Operator/CompleteCodomain.lean b/Mathlib/Analysis/Normed/Operator/CompleteCodomain.lean
index 158bddf9b3eed7..7d2fc86f6b4337 100644
--- a/Mathlib/Analysis/Normed/Operator/CompleteCodomain.lean
+++ b/Mathlib/Analysis/Normed/Operator/CompleteCodomain.lean
@@ -44,7 +44,7 @@ lemma completeSpace_of_completeSpace_continuousLinearMap [CompleteSpace (E →L[
   have : Tendsto (fun n ↦ g n v) atTop (𝓝 (a v)) := by
     have : Continuous (fun (i : E →L[𝕜] F) ↦ i v) := by fun_prop
     exact (this.tendsto _).comp ha
-  simpa [g, ContinuousLinearMap.smulRightL, hφ]
+  simpa [g, hφ]
 
 lemma completeSpace_continuousLinearMap_iff :
     CompleteSpace (E →L[𝕜] F) ↔ CompleteSpace F :=
diff --git a/Mathlib/Analysis/Normed/Operator/NormedSpace.lean b/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
index 91ea19160ef036..2bb9815405672a 100644
--- a/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
+++ b/Mathlib/Analysis/Normed/Operator/NormedSpace.lean
@@ -197,7 +197,7 @@ theorem norm_smulRightL (c : StrongDual 𝕜 E) [Nontrivial Fₗ] : ‖smulRight
   ContinuousLinearMap.homothety_norm _ c.norm_smulRight_apply
 
 lemma norm_smulRightL_le : ‖smulRightL 𝕜 E Fₗ‖ ≤ 1 :=
-  LinearMap.mkContinuous₂_norm_le _ zero_le_one _
+  ContinuousLinearMap.opNorm_le_bound₂ _ zero_le_one fun c x ↦ by simp
 
 /-! ### Composition with isometries -/
 
diff --git a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
index 37f2a3f8ade317..8d1366b0e46bda 100644
--- a/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
+++ b/Mathlib/Geometry/Manifold/IsManifold/Basic.lean
@@ -1041,7 +1041,7 @@ deriving
   ContinuousSMul 𝕜,
   -- the following instance derives from the previous one, but through an instance with priority 100
   -- which takes a long time to be found. We register a shortcut instance instead
-  ContinuousConstSMul 𝕜
+  ContinuousConstSMul 𝕜, IsNormableSpace 𝕜
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
index d923a7b19f7167..57620e90e968ce 100644
--- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
+++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 public import Mathlib.Analysis.LocallyConvex.Bounded
+public import Mathlib.Analysis.LocallyConvex.WithSeminorms
 public import Mathlib.Analysis.Normed.Module.Basic
 public import Mathlib.Analysis.SpecificLimits.Normed
 public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
@@ -601,6 +602,23 @@ theorem ContinuousLinearMap.isStrictMap_of_finiteDimensional [T2Space F] [Finite
   rw [isStrictMap_iff_isQuotientMap_rangeFactorization]
   exact f.rangeRestrict.isQuotientMap_of_finiteDimensional (by simp)
 
+variable (E) in
+private lemma isNormableSpace_of_t2Space_finiteDimensional
+    [T2Space E] [FiniteDimensional 𝕜 E] : IsNormableSpace 𝕜 E := by
+  have e : E ≃L[𝕜] (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜 :=
+    (Basis.ofVectorSpace 𝕜 E).equivFun.toContinuousLinearEquiv
+  exact e.isNormableSpace
+
+/-- A finite dimensional topological vector space over a complete normed field is normable.
+
+Not registered as a global instance only for performance reasons. -/
+theorem isNormableSpace_of_finiteDimensional [FiniteDimensional 𝕜 E] : IsNormableSpace 𝕜 E := by
+  let F := SeparationQuotient E
+  have : IsNormableSpace 𝕜 F := isNormableSpace_of_t2Space_finiteDimensional _
+  let f : E →ₗ[𝕜] F := SeparationQuotient.mkCLM 𝕜 E
+  have : IsInducing f := SeparationQuotient.isInducing_mk
+  exact this.isNormableSpace
+
 /-- If `K` is a complete field and `V` is a finite-dimensional vector space over `K` (equipped with
 any topology so that `V` is a topological `K`-module, meaning `[IsTopologicalAddGroup V]`
 and `[ContinuousSMul K V]`), and `K` is locally compact, then `V` is locally compact.
diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean b/Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean
index 28992ed2ec8585..406b522ef7d5a3 100644
--- a/Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean
+++ b/Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean
@@ -5,6 +5,7 @@ Authors: Patrick Massot, Michael Rothgang
 -/
 module
 
+public import Mathlib.Analysis.Normed.Operator.Bilinear
 public import Mathlib.Topology.Algebra.Module.FiniteDimension
 public import Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
 
@@ -14,8 +15,6 @@ public import Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
 Given a complete nontrivially normed field `𝕜` and finite dimensional T₂ topological vector spaces
 over `𝕜`, this file builds a continuous bilinear map from any bilinear function.
 
-This applies in particular to evaluation of linear maps between such spaces.
-
 Working with topological vector spaces instead of normed spaces is important for applications in the
 differential geometry part of Mathlib where we don’t want to fix a norm on tangent spaces for
 instance.
@@ -54,16 +53,7 @@ lemma IsBilinearMap.toContinuousBilinearMap_apply {f : E → F → G} (h : IsBil
     (x : E) (y : F) :
   h.toContinuousBilinearMap x y = f x y := rfl
 
-variable (𝕜 E F) in
-/-- Evaluation of continuous linear maps as a continuous linear map in the
-case of finite dimensional topological vector spaces over a complete field.
-See also `ContinuousLinearMap.apply` for the case of normed spaces.
-
-TODO: generalize the two constructions in the setting of maps from a bornological space to a locally
-convex one, or define a `NormableSpace` class to deduce this case from the normed case.
--/
-def ContinuousLinearMap.evalL : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F :=
-  LinearMap.toContinuousLinearMap.symm.toLinearMap |>.flip |>.toContinuousBilinearMap
+@[deprecated (since := "2026-08-21")] alias ContinuousLinearMap.evalL := ContinuousLinearMap.apply
 
-@[simp]
-lemma ContinuousLinearMap.evalL_apply (x : E) (φ : E →L[𝕜] F) : φ.evalL 𝕜 E F x = φ x := rfl
+@[deprecated (since := "2026-08-21")] alias ContinuousLinearMap.evalL_apply :=
+  ContinuousLinearMap.apply_apply