feat: NormedAlgebra.complexToReal and other RestrictScalars insta…

…nces (leanprover-community#10374)

This adds some instances regarding normed algebra structures to `RestrictScalars` to mimic those for normed spaces.

In addition, given a normed `ℂ`-algebra, this puts a normed `ℝ`-algebra structure on the same space. This is *not* adding any new data instances, as these already exist from `Algebra.complexToReal`.

Mathlib/Analysis/Complex/Basic.lean

@@ -81,14 +81,20 @@ instance {R : Type*} [NormedField R] [NormedAlgebra R ℝ] : NormedAlgebra R ℂ
     rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_eq_abs, abs_ofReal, ← Real.norm_eq_abs,
       norm_algebraMap']
 
-variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
+variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℂ E]
 
 -- see Note [lower instance priority]
 /-- The module structure from `Module.complexToReal` is a normed space. -/
 instance (priority := 900) _root_.NormedSpace.complexToReal : NormedSpace ℝ E :=
   NormedSpace.restrictScalars ℝ ℂ E
 #align normed_space.complex_to_real NormedSpace.complexToReal
 
+-- see Note [lower instance priority]
+/-- The algebra structure from `Algebra.complexToReal` is a normed algebra. -/
+instance (priority := 900) _root_.NormedAlgebra.complexToReal {A : Type*} [SeminormedRing A]
+    [NormedAlgebra ℂ A] : NormedAlgebra ℝ A :=
+  NormedAlgebra.restrictScalars ℝ ℂ A
+
 theorem dist_eq (z w : ℂ) : dist z w = abs (z - w) :=
   rfl
 #align complex.dist_eq Complex.dist_eq

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -414,17 +414,57 @@ instance Subalgebra.toNormedAlgebra {𝕜 A : Type*} [SeminormedRing A] [NormedF
 
 section RestrictScalars
 
-variable (𝕜 : Type*) (𝕜' : Type*) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
-  (E : Type*) [SeminormedAddCommGroup E] [NormedSpace 𝕜' E]
+section NormInstances
+
+variable {𝕜 𝕜' E : Type*}
 
-instance {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [I : SeminormedAddCommGroup E] :
+instance [I : SeminormedAddCommGroup E] :
     SeminormedAddCommGroup (RestrictScalars 𝕜 𝕜' E) :=
   I
 
-instance {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [I : NormedAddCommGroup E] :
+instance [I : NormedAddCommGroup E] :
     NormedAddCommGroup (RestrictScalars 𝕜 𝕜' E) :=
   I
 
+instance [I : NonUnitalSeminormedRing E] :
+    NonUnitalSeminormedRing (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+instance [I : NonUnitalNormedRing E] :
+    NonUnitalNormedRing (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+instance [I : SeminormedRing E] :
+    SeminormedRing (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+instance [I : NormedRing E] :
+    NormedRing (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+instance [I : NonUnitalSeminormedCommRing E] :
+    NonUnitalSeminormedCommRing (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+instance [I : NonUnitalNormedCommRing E] :
+    NonUnitalNormedCommRing (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+instance [I : SeminormedCommRing E] :
+    SeminormedCommRing (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+instance [I : NormedCommRing E] :
+    NormedCommRing (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+end NormInstances
+
+section NormedSpace
+
+variable (𝕜 : Type*) (𝕜' : Type*) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+  (E : Type*) [SeminormedAddCommGroup E] [NormedSpace 𝕜' E]
+
 /-- If `E` is a normed space over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
 `RestrictScalars.module` is additionally a `NormedSpace`. -/
 instance RestrictScalars.normedSpace : NormedSpace 𝕜 (RestrictScalars 𝕜 𝕜' E) :=
@@ -453,4 +493,38 @@ def NormedSpace.restrictScalars : NormedSpace 𝕜 E :=
   RestrictScalars.normedSpace _ 𝕜' _
 #align normed_space.restrict_scalars NormedSpace.restrictScalars
 
+end NormedSpace
+
+section NormedAlgebra
+
+variable (𝕜 : Type*) (𝕜' : Type*) [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+  (E : Type*) [SeminormedRing E] [NormedAlgebra 𝕜' E]
+
+/-- If `E` is a normed algebra over `𝕜'` and `𝕜` is a normed algebra over `𝕜'`, then
+`RestrictScalars.module` is additionally a `NormedAlgebra`. -/
+instance RestrictScalars.normedAlgebra : NormedAlgebra 𝕜 (RestrictScalars 𝕜 𝕜' E) :=
+  { RestrictScalars.algebra 𝕜 𝕜' E with
+    norm_smul_le := norm_smul_le }
+
+-- If you think you need this, consider instead reproducing `RestrictScalars.lsmul`
+-- appropriately modified here.
+/-- The action of the original normed_field on `RestrictScalars 𝕜 𝕜' E`.
+This is not an instance as it would be contrary to the purpose of `RestrictScalars`.
+-/
+def Module.RestrictScalars.normedAlgebraOrig {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [NormedField 𝕜']
+    [SeminormedRing E] [I : NormedAlgebra 𝕜' E] : NormedAlgebra 𝕜' (RestrictScalars 𝕜 𝕜' E) :=
+  I
+
+/-- Warning: This declaration should be used judiciously.
+Please consider using `IsScalarTower` and/or `RestrictScalars 𝕜 𝕜' E` instead.
+
+This definition allows the `RestrictScalars.normedAlgebra` instance to be put directly on `E`
+rather on `RestrictScalars 𝕜 𝕜' E`. This would be a very bad instance; both because `𝕜'` cannot be
+inferred, and because it is likely to create instance diamonds.
+-/
+def NormedAlgebra.restrictScalars : NormedAlgebra 𝕜 E :=
+  RestrictScalars.normedAlgebra _ 𝕜' _
+
+end NormedAlgebra
+
 end RestrictScalars