chore(Normed/Operator): add smulRightL_apply_apply (#31642)

Author: urkud

Mathlib/Analysis/Calculus/ParametricIntegral.lean

@@ -268,10 +268,7 @@ theorem hasDerivAt_integral_of_dominated_loc_of_lip {F' : α → E} (ε_pos : 0
     ε_pos hF_meas hF_int hm h_lipsch bound_integrable h_diff
   replace hF'_int : Integrable F' μ := by
     rw [← integrable_norm_iff hm] at hF'_int
-    simpa only [L, (· ∘ ·), integrable_norm_iff, hF'_meas, one_mul, norm_one,
-      ContinuousLinearMap.comp_apply, ContinuousLinearMap.coe_restrict_scalarsL',
-      ContinuousLinearMap.norm_restrictScalars, ContinuousLinearMap.norm_smulRightL_apply] using
-      hF'_int
+    simpa [L, (· ∘ ·), integrable_norm_iff hF'_meas] using hF'_int
   refine ⟨hF'_int, ?_⟩
   by_cases hE : CompleteSpace E; swap
   · simpa [integral, hE] using hasDerivAt_const x₀ 0

Mathlib/Analysis/Normed/Operator/Bilinear.lean

@@ -402,6 +402,7 @@ theorem nnnorm_smulRight_apply (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRight
 variable (𝕜 E Fₗ) in
 /-- `ContinuousLinearMap.smulRight` as a continuous trilinear map:
 `smulRightL (c : StrongDual 𝕜 E) (f : F) (x : E) = c x • f`. -/
+@[simps! apply_apply]
 def smulRightL : StrongDual 𝕜 E →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ :=
   LinearMap.mkContinuous₂
     { toFun := smulRightₗ
@@ -416,10 +417,10 @@ 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]
-theorem norm_smulRightL_apply (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRightL 𝕜 E Fₗ c f‖ = ‖c‖ * ‖f‖ :=
-  norm_smulRight_apply c f
+@[deprecated norm_smulRight_apply (since := "2025-11-12")]
+theorem norm_smulRightL_apply (c : StrongDual 𝕜 E) (f : Fₗ) :
+    ‖smulRightL 𝕜 E Fₗ c f‖ = ‖c‖ * ‖f‖ := by
+  simp
 
 end ContinuousLinearMap