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..24a773443234d1 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_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_apply (c : StrongDual 𝕜 E) (x) :
+    c.smulRightₗ' 𝕜 E F x = c.smulRight x := rfl
+@[simp] lemma toLinearMap_smulRightₗ'_apply (c : StrongDual 𝕜 E) :
+    (c.smulRightₗ' 𝕜 E F).toLinearMap = c.smulRightₗ := rfl
+
 end ContinuousLinearMap
 
 open ContinuousLinearMap