From fa3a46aaf61e99b184e550713f322dbfef9ac4d9 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Tue, 25 Aug 2026 20:15:58 +0100
Subject: [PATCH 1/2] smulRightL as a linear map

---
 .../Analysis/Normed/Operator/Bilinear.lean    |  2 ++
 .../Module/Spaces/ContinuousLinearMap.lean    | 19 ++++++++++++++++++-
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Normed/Operator/Bilinear.lean b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
index cc464034a7b100..fe48b9e039621a 100644
--- a/Mathlib/Analysis/Normed/Operator/Bilinear.lean
+++ b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
@@ -437,6 +437,8 @@ def smulRightL : StrongDual 𝕜 E →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ
       simp only [coe_smulRightₗ, one_mul, norm_smulRight_apply, LinearMap.coe_mk, AddHom.coe_mk,
         le_refl]
 
+@[simp] lemma toLinearMap_smulRightL : (smulRightL 𝕜 E Fₗ).toLinearMap = smulRightₗ' 𝕜 E Fₗ := rfl
+
 end ContinuousLinearMap
 
 end SemiNormed
diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 105cf6b50e641e..42166755b081b7 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -470,8 +470,9 @@ def prodL : ((E →L[𝕜] F) × (E →L[𝕜] G)) ≃L[S] (E →L[𝕜] F × G)
 end Prod
 
 variable {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
-  [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
+  [TopologicalSpace E]
 
+variable [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] in
 /-- `ContinuousLinearMap.toSpanSingleton` as a continuous linear equivalence. -/
 @[simps!]
 def toSpanSingletonCLE : E ≃L[𝕜] (𝕜 →L[𝕜] E) where
@@ -480,6 +481,22 @@ def toSpanSingletonCLE : E ≃L[𝕜] (𝕜 →L[𝕜] E) where
     continuous_snd.smul continuous_fst
   continuous_invFun := continuous_eval_const 1
 
+variable {F : Type*} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
+  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F]
+
+variable (𝕜 E F) in
+/-- `smulRight` as a partly continuous trilinear map.
+This is the bundled continuous version of `smulRightₗ`. -/
+@[simps! apply_apply] def smulRightₗ' : StrongDual 𝕜 E →ₗ[𝕜] (F →L[𝕜] E →L[𝕜] F) where
+  toFun c := (c.precomp F) ∘SL toSpanSingletonCLE.toContinuousLinearMap
+  map_add' _ _ := by ext; simp
+  map_smul' _ _ := by ext; simp
+
+@[simp] lemma smulRightₗ'_apply (c : StrongDual 𝕜 E) (x) :
+    c.smulRightₗ' 𝕜 E F x = c.smulRight x := rfl
+@[simp] lemma toLinearMap_smulRightₗ' (c : StrongDual 𝕜 E) :
+    (c.smulRightₗ' 𝕜 E F).toLinearMap = c.smulRightₗ := rfl
+
 end ContinuousLinearMap
 
 open ContinuousLinearMap

From c6f0c9df69b5faf3e9f8a2d70a705a0006a2d9f5 Mon Sep 17 00:00:00 2001
From: Monica Omar <23701951+themathqueen@users.noreply.github.com>
Date: Tue, 25 Aug 2026 20:19:39 +0100
Subject: [PATCH 2/2] fix

---
 .../Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 42166755b081b7..24a773443234d1 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -487,14 +487,14 @@ variable {F : Type*} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
 variable (𝕜 E F) in
 /-- `smulRight` as a partly continuous trilinear map.
 This is the bundled continuous version of `smulRightₗ`. -/
-@[simps! apply_apply] def smulRightₗ' : StrongDual 𝕜 E →ₗ[𝕜] (F →L[𝕜] E →L[𝕜] F) where
+@[simps! apply_apply_apply] def smulRightₗ' : StrongDual 𝕜 E →ₗ[𝕜] (F →L[𝕜] E →L[𝕜] F) where
   toFun c := (c.precomp F) ∘SL toSpanSingletonCLE.toContinuousLinearMap
   map_add' _ _ := by ext; simp
   map_smul' _ _ := by ext; simp
 
-@[simp] lemma smulRightₗ'_apply (c : StrongDual 𝕜 E) (x) :
+@[simp] lemma smulRightₗ'_apply_apply (c : StrongDual 𝕜 E) (x) :
     c.smulRightₗ' 𝕜 E F x = c.smulRight x := rfl
-@[simp] lemma toLinearMap_smulRightₗ' (c : StrongDual 𝕜 E) :
+@[simp] lemma toLinearMap_smulRightₗ'_apply (c : StrongDual 𝕜 E) :
     (c.smulRightₗ' 𝕜 E F).toLinearMap = c.smulRightₗ := rfl
 
 end ContinuousLinearMap