chore(Analysis/NormedSpace/OperatorNorm/Mul): don't use 𝕜' for a ring (#21506)

I am finding it particularly confusing to use `𝕜something` for a ring when `𝕜` is already used for a type playing a completely different role.

From LeanAPAP

Author: YaelDillies

Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean

@@ -30,68 +30,68 @@ section MultiplicationLinear
 
 section NonUnital
 
-variable (𝕜) (𝕜' : Type*) [NonUnitalSeminormedRing 𝕜']
-variable [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜']
+variable (𝕜) (R : Type*) [NonUnitalSeminormedRing R]
+variable [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R]
 
 /-- Multiplication in a non-unital normed algebra as a continuous bilinear map. -/
-def mul : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-  (LinearMap.mul 𝕜 𝕜').mkContinuous₂ 1 fun x y => by simpa using norm_mul_le x y
+def mul : R →L[𝕜] R →L[𝕜] R :=
+  (LinearMap.mul 𝕜 R).mkContinuous₂ 1 fun x y => by simpa using norm_mul_le x y
 
 @[simp]
-theorem mul_apply' (x y : 𝕜') : mul 𝕜 𝕜' x y = x * y :=
+theorem mul_apply' (x y : R) : mul 𝕜 R x y = x * y :=
   rfl
 
 @[simp]
-theorem opNorm_mul_apply_le (x : 𝕜') : ‖mul 𝕜 𝕜' x‖ ≤ ‖x‖ :=
+theorem opNorm_mul_apply_le (x : R) : ‖mul 𝕜 R x‖ ≤ ‖x‖ :=
   opNorm_le_bound _ (norm_nonneg x) (norm_mul_le x)
 
 
-theorem opNorm_mul_le : ‖mul 𝕜 𝕜'‖ ≤ 1 :=
+theorem opNorm_mul_le : ‖mul 𝕜 R‖ ≤ 1 :=
   LinearMap.mkContinuous₂_norm_le _ zero_le_one _
 
 
-/-- Multiplication on the left in a non-unital normed algebra `𝕜'` as a non-unital algebra
+/-- Multiplication on the left in a non-unital normed algebra `R` as a non-unital algebra
 homomorphism into the algebra of *continuous* linear maps. This is the left regular representation
 of `A` acting on itself.
 
 This has more algebraic structure than `ContinuousLinearMap.mul`, but there is no longer continuity
 bundled in the first coordinate.  An alternative viewpoint is that this upgrades
 `NonUnitalAlgHom.lmul` from a homomorphism into linear maps to a homomorphism into *continuous*
 linear maps. -/
-def _root_.NonUnitalAlgHom.Lmul : 𝕜' →ₙₐ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-  { mul 𝕜 𝕜' with
+def _root_.NonUnitalAlgHom.Lmul : R →ₙₐ[𝕜] R →L[𝕜] R :=
+  { mul 𝕜 R with
     map_mul' := fun _ _ ↦ ext fun _ ↦ mul_assoc _ _ _
     map_zero' := ext fun _ ↦ zero_mul _ }
 
-variable {𝕜 𝕜'} in
+variable {𝕜 R} in
 @[simp]
-theorem _root_.NonUnitalAlgHom.coe_Lmul : ⇑(NonUnitalAlgHom.Lmul 𝕜 𝕜') = mul 𝕜 𝕜' :=
+theorem _root_.NonUnitalAlgHom.coe_Lmul : ⇑(NonUnitalAlgHom.Lmul 𝕜 R) = mul 𝕜 R :=
   rfl
 
 /-- Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a
 continuous trilinear map. This is akin to its non-continuous version `LinearMap.mulLeftRight`,
 but there is a minor difference: `LinearMap.mulLeftRight` is uncurried. -/
-def mulLeftRight : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-  ((compL 𝕜 𝕜' 𝕜' 𝕜').comp (mul 𝕜 𝕜').flip).flip.comp (mul 𝕜 𝕜')
+def mulLeftRight : R →L[𝕜] R →L[𝕜] R →L[𝕜] R :=
+  ((compL 𝕜 R R R).comp (mul 𝕜 R).flip).flip.comp (mul 𝕜 R)
 
 @[simp]
-theorem mulLeftRight_apply (x y z : 𝕜') : mulLeftRight 𝕜 𝕜' x y z = x * z * y :=
+theorem mulLeftRight_apply (x y z : R) : mulLeftRight 𝕜 R x y z = x * z * y :=
   rfl
 
-theorem opNorm_mulLeftRight_apply_apply_le (x y : 𝕜') : ‖mulLeftRight 𝕜 𝕜' x y‖ ≤ ‖x‖ * ‖y‖ :=
+theorem opNorm_mulLeftRight_apply_apply_le (x y : R) : ‖mulLeftRight 𝕜 R x y‖ ≤ ‖x‖ * ‖y‖ :=
   (opNorm_comp_le _ _).trans <|
     (mul_comm _ _).trans_le <|
       mul_le_mul (opNorm_mul_apply_le _ _ _)
         (opNorm_le_bound _ (norm_nonneg _) fun _ => (norm_mul_le _ _).trans_eq (mul_comm _ _))
         (norm_nonneg _) (norm_nonneg _)
 
-theorem opNorm_mulLeftRight_apply_le (x : 𝕜') : ‖mulLeftRight 𝕜 𝕜' x‖ ≤ ‖x‖ :=
-  opNorm_le_bound _ (norm_nonneg x) (opNorm_mulLeftRight_apply_apply_le 𝕜 𝕜' x)
+theorem opNorm_mulLeftRight_apply_le (x : R) : ‖mulLeftRight 𝕜 R x‖ ≤ ‖x‖ :=
+  opNorm_le_bound _ (norm_nonneg x) (opNorm_mulLeftRight_apply_apply_le 𝕜 R x)
 
 set_option maxSynthPendingDepth 2 in
 theorem opNorm_mulLeftRight_le :
-    ‖mulLeftRight 𝕜 𝕜'‖ ≤ 1 :=
-  opNorm_le_bound _ zero_le_one fun x => (one_mul ‖x‖).symm ▸ opNorm_mulLeftRight_apply_le 𝕜 𝕜' x
+    ‖mulLeftRight 𝕜 R‖ ≤ 1 :=
+  opNorm_le_bound _ zero_le_one fun x => (one_mul ‖x‖).symm ▸ opNorm_mulLeftRight_apply_le 𝕜 R x
 
 
 /-- This is a mixin class for non-unital normed algebras which states that the left-regular
@@ -104,39 +104,39 @@ This is a useful class because it gives rise to a nice norm on the unitization;
 a C⋆-norm when the norm on `A` is a C⋆-norm. -/
 class _root_.RegularNormedAlgebra : Prop where
   /-- The left regular representation of the algebra on itself is an isometry. -/
-  isometry_mul' : Isometry (mul 𝕜 𝕜')
+  isometry_mul' : Isometry (mul 𝕜 R)
 
 /-- Every (unital) normed algebra such that `‖1‖ = 1` is a `RegularNormedAlgebra`. -/
-instance _root_.NormedAlgebra.instRegularNormedAlgebra {𝕜 𝕜' : Type*} [NontriviallyNormedField 𝕜]
-    [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : RegularNormedAlgebra 𝕜 𝕜' where
-  isometry_mul' := AddMonoidHomClass.isometry_of_norm (mul 𝕜 𝕜') <|
+instance _root_.NormedAlgebra.instRegularNormedAlgebra {𝕜 R : Type*} [NontriviallyNormedField 𝕜]
+    [SeminormedRing R] [NormedAlgebra 𝕜 R] [NormOneClass R] : RegularNormedAlgebra 𝕜 R where
+  isometry_mul' := AddMonoidHomClass.isometry_of_norm (mul 𝕜 R) <|
     fun x => le_antisymm (opNorm_mul_apply_le _ _ _) <| by
-      convert ratio_le_opNorm ((mul 𝕜 𝕜') x) (1 : 𝕜')
+      convert ratio_le_opNorm ((mul 𝕜 R) x) (1 : R)
       simp [norm_one]
 
-variable [RegularNormedAlgebra 𝕜 𝕜']
+variable [RegularNormedAlgebra 𝕜 R]
 
-lemma isometry_mul : Isometry (mul 𝕜 𝕜') :=
+lemma isometry_mul : Isometry (mul 𝕜 R) :=
   RegularNormedAlgebra.isometry_mul'
 
 @[simp]
-lemma opNorm_mul_apply (x : 𝕜') : ‖mul 𝕜 𝕜' x‖ = ‖x‖ :=
-  (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 𝕜')).mp (isometry_mul 𝕜 𝕜') x
+lemma opNorm_mul_apply (x : R) : ‖mul 𝕜 R x‖ = ‖x‖ :=
+  (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 R)).mp (isometry_mul 𝕜 R) x
 
 
 @[simp]
-lemma opNNNorm_mul_apply (x : 𝕜') : ‖mul 𝕜 𝕜' x‖₊ = ‖x‖₊ :=
-  Subtype.ext <| opNorm_mul_apply 𝕜 𝕜' x
+lemma opNNNorm_mul_apply (x : R) : ‖mul 𝕜 R x‖₊ = ‖x‖₊ :=
+  Subtype.ext <| opNorm_mul_apply 𝕜 R x
 
 
 /-- Multiplication in a normed algebra as a linear isometry to the space of
 continuous linear maps. -/
-def mulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' where
-  toLinearMap := mul 𝕜 𝕜'
-  norm_map' x := opNorm_mul_apply 𝕜 𝕜' x
+def mulₗᵢ : R →ₗᵢ[𝕜] R →L[𝕜] R where
+  toLinearMap := mul 𝕜 R
+  norm_map' x := opNorm_mul_apply 𝕜 R x
 
 @[simp]
-theorem coe_mulₗᵢ : ⇑(mulₗᵢ 𝕜 𝕜') = mul 𝕜 𝕜' :=
+theorem coe_mulₗᵢ : ⇑(mulₗᵢ 𝕜 R) = mul 𝕜 R :=
   rfl
 
 end NonUnital
@@ -180,19 +180,19 @@ end MultiplicationLinear
 
 section SMulLinear
 
-variable (𝕜) (𝕜' : Type*) [NormedField 𝕜']
-variable [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E]
+variable (𝕜) (R : Type*) [NormedField R]
+variable [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E]
 
 /-- Scalar multiplication as a continuous bilinear map. -/
-def lsmul : 𝕜' →L[𝕜] E →L[𝕜] E :=
-  ((Algebra.lsmul 𝕜 𝕜 E).toLinearMap : 𝕜' →ₗ[𝕜] E →ₗ[𝕜] E).mkContinuous₂ 1 fun c x => by
+def lsmul : R →L[𝕜] E →L[𝕜] E :=
+  ((Algebra.lsmul 𝕜 𝕜 E).toLinearMap : R →ₗ[𝕜] E →ₗ[𝕜] E).mkContinuous₂ 1 fun c x => by
     simpa only [one_mul] using norm_smul_le c x
 
 @[simp]
-theorem lsmul_apply (c : 𝕜') (x : E) : lsmul 𝕜 𝕜' c x = c • x :=
+theorem lsmul_apply (c : R) (x : E) : lsmul 𝕜 R c x = c • x :=
   rfl
 
-variable {𝕜'}
+variable {R}
 
 theorem norm_toSpanSingleton (x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖ := by
   refine opNorm_eq_of_bounds (norm_nonneg _) (fun x => ?_) fun N _ h => ?_
@@ -203,12 +203,12 @@ theorem norm_toSpanSingleton (x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖ :=
 
 variable {𝕜}
 
-theorem opNorm_lsmul_apply_le (x : 𝕜') : ‖(lsmul 𝕜 𝕜' x : E →L[𝕜] E)‖ ≤ ‖x‖ :=
+theorem opNorm_lsmul_apply_le (x : R) : ‖(lsmul 𝕜 R x : E →L[𝕜] E)‖ ≤ ‖x‖ :=
   ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg x) fun y => norm_smul_le x y
 
 
 /-- The norm of `lsmul` is at most 1 in any semi-normed group. -/
-theorem opNorm_lsmul_le : ‖(lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] E →L[𝕜] E)‖ ≤ 1 := by
+theorem opNorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ ≤ 1 := by
   refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun x => ?_
   simp_rw [one_mul]
   exact opNorm_lsmul_apply_le _
@@ -225,21 +225,21 @@ section Normed
 namespace ContinuousLinearMap
 
 variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-variable (𝕜) (𝕜' : Type*)
+variable (𝕜) (R : Type*)
 
 section
 
-variable [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜']
-variable [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜']
+variable [NonUnitalNormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R]
+variable [SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R] [Nontrivial R]
 
 @[simp]
-theorem opNorm_mul : ‖mul 𝕜 𝕜'‖ = 1 :=
-  (mulₗᵢ 𝕜 𝕜').norm_toContinuousLinearMap
+theorem opNorm_mul : ‖mul 𝕜 R‖ = 1 :=
+  (mulₗᵢ 𝕜 R).norm_toContinuousLinearMap
 
 
 @[simp]
-theorem opNNNorm_mul : ‖mul 𝕜 𝕜'‖₊ = 1 :=
-  Subtype.ext <| opNorm_mul 𝕜 𝕜'
+theorem opNNNorm_mul : ‖mul 𝕜 R‖₊ = 1 :=
+  Subtype.ext <| opNorm_mul 𝕜 R
 
 
 end
@@ -248,8 +248,8 @@ end
 
 This is `ContinuousLinearMap.opNorm_lsmul_le` as an equality. -/
 @[simp]
-theorem opNorm_lsmul [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E]
-    [IsScalarTower 𝕜 𝕜' E] [Nontrivial E] : ‖(lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] E →L[𝕜] E)‖ = 1 := by
+theorem opNorm_lsmul [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E]
+    [IsScalarTower 𝕜 R E] [Nontrivial E] : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ = 1 := by
   refine ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one (fun x => ?_) fun N _ h => ?_
   · rw [one_mul]
     apply opNorm_lsmul_apply_le