refactor(Analysis): golf Mathlib/Analysis/Normed/Operator/Mul

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -795,8 +795,8 @@ lemma hasDerivAt_fourier
   have h_int : Integrable fun v ↦ fourierSMulRight L f v := by
     suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
       simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)
-    convert ((ContinuousLinearMap.ring_lmap_equiv_self ℝ
-      E).symm.toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v
+    convert ((ContinuousLinearMap.toSpanSingletonₗᵢ ℝ
+      E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v
     apply ContinuousLinearMap.ext_ring
     rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
       ContinuousLinearMap.mul_apply', one_mul, map_smul]

Mathlib/Analysis/Normed/Operator/Mul.lean

@@ -156,26 +156,29 @@ section RingEquiv
 
 variable (𝕜 E)
 
-/-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly equivalent
-to `M`. (See `ring_lmap_equiv_self` for a stronger statement.) -/
-def ring_lmap_equiv_selfₗ : (𝕜 →L[𝕜] E) ≃ₗ[𝕜] E where
-  toFun := fun f ↦ f 1
-  invFun := (ContinuousLinearMap.id 𝕜 𝕜).smulRight
-  map_smul' := fun a f ↦ by simp only [coe_smul', Pi.smul_apply, RingHom.id_apply]
-  map_add' := fun f g ↦ by simp only [add_apply]
-  left_inv := fun f ↦ by ext; simp only [smulRight_apply, coe_id', _root_.id, one_smul]
-  right_inv := fun m ↦ by simp only [smulRight_apply, id_apply, one_smul]
-
 /-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly isometrically
 equivalent to `M`. -/
-def ring_lmap_equiv_self : (𝕜 →L[𝕜] E) ≃ₗᵢ[𝕜] E where
-  toLinearEquiv := ring_lmap_equiv_selfₗ 𝕜 E
-  norm_map' := by
-    refine fun f ↦ le_antisymm ?_ ?_
-    · simpa only [norm_one, mul_one] using le_opNorm f 1
-    · refine opNorm_le_bound' f (norm_nonneg <| f 1) (fun x _ ↦ ?_)
-      rw [(by rw [smul_eq_mul, mul_one] : f x = f (x • 1)), map_smul,
-        norm_smul, mul_comm, (by rfl : ring_lmap_equiv_selfₗ 𝕜 E f = f 1)]
+@[simp]
+def toSpanSingletonₗᵢ : E ≃ₗᵢ[𝕜] (𝕜 →L[𝕜] E) where
+  toLinearEquiv := toSpanSingletonLE 𝕜 𝕜 E
+  norm_map' _ := by simp
+
+lemma toSpanSingletonₗᵢ_apply (x : E) : toSpanSingletonₗᵢ 𝕜 E x = toSpanSingletonLE 𝕜 𝕜 E x := by
+  simp
+
+lemma toSpanSingletonₗᵢ_symm_apply (f : 𝕜 →L[𝕜] E) :
+    (toSpanSingletonₗᵢ 𝕜 E).symm f = (toSpanSingletonLE 𝕜 𝕜 E).symm f :=
+  Eq.symm (DFunLike.congr_fun rfl f)
+
+lemma toSpanSingletonₗᵢ_toLinearEquiv :
+    (toSpanSingletonₗᵢ 𝕜 E).toLinearEquiv = toSpanSingletonLE 𝕜 𝕜 E := by
+  simp
+
+@[deprecated (since := "2026-04-23")]
+alias ring_lmap_equiv_selfₗ := toSpanSingletonLE
+
+@[deprecated (since := "2026-04-23")]
+alias ring_lmap_equiv_self := toSpanSingletonₗᵢ
 
 end RingEquiv
 

Mathlib/Topology/Algebra/Module/LinearMap.lean

@@ -1096,7 +1096,8 @@ variable (R S M : Type*) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M
   [SMulCommClass R S M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul S M]
   [TopologicalSpace R] [ContinuousSMul R M]
 
-/-- `ContinuousLinearMap.toSpanSingleton` as a linear equivalence. -/
+/-- `ContinuousLinearMap.toSpanSingleton` as a linear equivalence. See
+`ContinuousLinearMap.toSpanSingletonₗᵢ` for a stronger statement. -/
 @[simps -fullyApplied]
 def toSpanSingletonLE : M ≃ₗ[S] (R →L[R] M) where
   toFun := toSpanSingleton R