chore(Analysis/NormedSpace/ContinuousLinearMap): forward-port leanpro…

…ver-community/mathlib#19108 (#6217)

Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

@@ -5,7 +5,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 -/
 import Mathlib.Analysis.NormedSpace.Basic
 
-#align_import analysis.normed_space.continuous_linear_map from "leanprover-community/mathlib"@"41bef4ae1254365bc190aee63b947674d2977f01"
+#align_import analysis.normed_space.continuous_linear_map from "leanprover-community/mathlib"@"fe18deda804e30c594e75a6e5fe0f7d14695289f"
 
 /-! # Constructions of continuous linear maps between (semi-)normed spaces
 
@@ -35,16 +35,15 @@ open NNReal
 
 variable {𝕜 𝕜₂ E F G : Type _}
 
-variable [NormedField 𝕜] [NormedField 𝕜₂]
-
 /-! # General constructions -/
 
+section SeminormedAddCommGroup
 
-section Seminormed
+variable [Ring 𝕜] [Ring 𝕜₂]
 
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G]
 
-variable [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 G]
+variable [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 G]
 
 variable {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F)
 
@@ -55,16 +54,6 @@ def LinearMap.mkContinuous (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : E
   ⟨f, AddMonoidHomClass.continuous_of_bound f C h⟩
 #align linear_map.mk_continuous LinearMap.mkContinuous
 
-/-- Reinterpret a linear map `𝕜 →ₗ[𝕜] E` as a continuous linear map. This construction
-is generalized to the case of any finite dimensional domain
-in `LinearMap.toContinuousLinearMap`. -/
-def LinearMap.toContinuousLinearMap₁ (f : 𝕜 →ₗ[𝕜] E) : 𝕜 →L[𝕜] E :=
-  f.mkContinuous ‖f 1‖ fun x =>
-    le_of_eq <| by
-      conv_lhs => rw [← mul_one x]
-      rw [← smul_eq_mul, f.map_smul, norm_smul, mul_comm]
-#align linear_map.to_continuous_linear_map₁ LinearMap.toContinuousLinearMap₁
-
 /-- Construct a continuous linear map from a linear map and the existence of a bound on this linear
 map. If you have an explicit bound, use `LinearMap.mkContinuous` instead, as a norm estimate will
 follow automatically in `LinearMap.mkContinuous_norm_le`. -/
@@ -118,18 +107,6 @@ theorem LinearMap.mkContinuousOfExistsBound_apply (h : ∃ C, ∀ x, ‖f x‖ 
   rfl
 #align linear_map.mk_continuous_of_exists_bound_apply LinearMap.mkContinuousOfExistsBound_apply
 
-@[simp]
-theorem LinearMap.toContinuousLinearMap₁_coe (f : 𝕜 →ₗ[𝕜] E) :
-    (f.toContinuousLinearMap₁ : 𝕜 →ₗ[𝕜] E) = f :=
-  rfl
-#align linear_map.to_continuous_linear_map₁_coe LinearMap.toContinuousLinearMap₁_coe
-
-@[simp]
-theorem LinearMap.toContinuousLinearMap₁_apply (f : 𝕜 →ₗ[𝕜] E) (x) :
-    f.toContinuousLinearMap₁ x = f x :=
-  rfl
-#align linear_map.to_continuous_linear_map₁_apply LinearMap.toContinuousLinearMap₁_apply
-
 namespace ContinuousLinearMap
 
 theorem antilipschitz_of_bound (f : E →SL[σ] F) {K : ℝ≥0} (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) :
@@ -159,12 +136,38 @@ def LinearEquiv.toContinuousLinearEquivOfBounds (e : E ≃ₛₗ[σ] F) (C_to C_
 
 end
 
-end Seminormed
+end SeminormedAddCommGroup
 
-section Normed
+section SeminormedBounded
+variable [SeminormedRing 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E]
+variable [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
+/-- Reinterpret a linear map `𝕜 →ₗ[𝕜] E` as a continuous linear map. This construction
+is generalized to the case of any finite dimensional domain
+in `LinearMap.toContinuousLinearMap`. -/
+def LinearMap.toContinuousLinearMap₁ (f : 𝕜 →ₗ[𝕜] E) : 𝕜 →L[𝕜] E :=
+  f.mkContinuous ‖f 1‖ fun x => by
+    conv_lhs => rw [← mul_one x]
+    rw [← smul_eq_mul, f.map_smul, mul_comm]; exact norm_smul_le _ _
+#align linear_map.to_continuous_linear_map₁ LinearMap.toContinuousLinearMap₁
 
-variable [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F]
+@[simp]
+theorem LinearMap.toContinuousLinearMap₁_coe (f : 𝕜 →ₗ[𝕜] E) :
+    (f.toContinuousLinearMap₁ : 𝕜 →ₗ[𝕜] E) = f :=
+  rfl
+#align linear_map.to_continuous_linear_map₁_coe LinearMap.toContinuousLinearMap₁_coe
 
+@[simp]
+theorem LinearMap.toContinuousLinearMap₁_apply (f : 𝕜 →ₗ[𝕜] E) (x) :
+    f.toContinuousLinearMap₁ x = f x :=
+  rfl
+#align linear_map.to_continuous_linear_map₁_apply LinearMap.toContinuousLinearMap₁_apply
+
+end SeminormedBounded
+
+section Normed
+variable [Ring 𝕜] [Ring 𝕜₂]
+variable [NormedAddCommGroup E] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F]
 variable {σ : 𝕜 →+* 𝕜₂} (f g : E →SL[σ] F) (x y z : E)
 
 theorem ContinuousLinearMap.uniformEmbedding_of_bound {K : ℝ≥0} (hf : ∀ x, ‖x‖ ≤ K * ‖f x‖) :
@@ -176,13 +179,10 @@ end Normed
 
 /-! ## Homotheties -/
 
-
 section Seminormed
-
+variable [Ring 𝕜] [Ring 𝕜₂]
 variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F]
-
-variable [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F]
-
+variable [Module 𝕜 E] [Module 𝕜₂ F]
 variable {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F)
 
 /-- A (semi-)linear map which is a homothety is a continuous linear map.
@@ -218,47 +218,40 @@ end Seminormed
 
 /-! ## The span of a single vector -/
 
-
-section Seminormed
-
-variable [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
-
 namespace ContinuousLinearMap
 
 variable (𝕜)
 
+section Seminormed
+
+variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
 theorem toSpanSingleton_homothety (x : E) (c : 𝕜) :
     ‖LinearMap.toSpanSingleton 𝕜 E x c‖ = ‖x‖ * ‖c‖ := by
   rw [mul_comm]
   exact norm_smul _ _
 #align continuous_linear_map.to_span_singleton_homothety ContinuousLinearMap.toSpanSingleton_homothety
 
-end ContinuousLinearMap
+end Seminormed
 
-section
+end ContinuousLinearMap
 
 namespace ContinuousLinearEquiv
 
 variable (𝕜)
 
+section Seminormed
+variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
 theorem toSpanNonzeroSingleton_homothety (x : E) (h : x ≠ 0) (c : 𝕜) :
     ‖LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h c‖ = ‖x‖ * ‖c‖ :=
   ContinuousLinearMap.toSpanSingleton_homothety _ _ _
 #align continuous_linear_equiv.to_span_nonzero_singleton_homothety ContinuousLinearEquiv.toSpanNonzeroSingleton_homothety
 
-end ContinuousLinearEquiv
-
-end
-
 end Seminormed
 
 section Normed
-
-variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-
-namespace ContinuousLinearEquiv
-
-variable (𝕜)
+variable [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 /-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural
     continuous linear equivalence from `E₁` to the span of `x`.-/
@@ -297,6 +290,6 @@ theorem coord_self (x : E) (h : x ≠ 0) :
   LinearEquiv.coord_self 𝕜 E x h
 #align continuous_linear_equiv.coord_self ContinuousLinearEquiv.coord_self
 
-end ContinuousLinearEquiv
-
 end Normed
+
+end ContinuousLinearEquiv