refactor(*): use is_scalar_tower instead of restrict_scalars (#4733)

- rename `semimodule.restrict_scalars` to `restrict_scalars`
- rename `restrict_scalars` to `subspace.restrict_scalars`
- use `is_scalar_tower` wherever possible
- add warnings to docstrings about `restrict_scalars` to encourage `is_scalar_tower` instead

Author: jcommelin

src/algebra/algebra/basic.lean

@@ -375,32 +375,35 @@ section
 local attribute [reducible] monoid_algebra
 
 variables (k)
+-- TODO: generalise from groups `G` to monoids
 /-- When `V` is a `k[G]`-module, multiplication by a group element `g` is a `k`-linear map. -/
 def group_smul.linear_map [group G] [comm_ring k]
-  (V : Type u₃) [add_comm_group V] [module (monoid_algebra k G) V] (g : G) :
-  (semimodule.restrict_scalars k (monoid_algebra k G) V) →ₗ[k]
-  (semimodule.restrict_scalars k (monoid_algebra k G) V) :=
+  (V : Type u₃) [add_comm_group V] [module k V] [module (monoid_algebra k G) V]
+  [is_scalar_tower k (monoid_algebra k G) V] (g : G) :
+  V →ₗ[k] V :=
 { to_fun    := λ v, (single g (1 : k) • v : V),
   map_add'  := λ x y, smul_add (single g (1 : k)) x y,
-  map_smul' := λ c x,
-  by simp only [semimodule.restrict_scalars_smul_def, coe_algebra_map, ←mul_smul, single_one_comm], }.
+  map_smul' := λ c x, smul_algebra_smul_comm _ _ _ }
 
 @[simp]
 lemma group_smul.linear_map_apply [group G] [comm_ring k]
-  (V : Type u₃) [add_comm_group V] [module (monoid_algebra k G) V] (g : G) (v : V) :
+  (V : Type u₃) [add_comm_group V] [module k V] [module (monoid_algebra k G) V]
+  [is_scalar_tower k (monoid_algebra k G) V] (g : G) (v : V) :
   (group_smul.linear_map k V g) v = (single g (1 : k) • v : V) :=
 rfl
 
 section
 variables {k}
-variables [group G] [comm_ring k]
-  {V : Type u₃} {gV : add_comm_group V} {mV : module (monoid_algebra k G) V}
-  {W : Type u₃} {gW : add_comm_group W} {mW : module (monoid_algebra k G) W}
-  (f : (semimodule.restrict_scalars k (monoid_algebra k G) V) →ₗ[k]
-       (semimodule.restrict_scalars k (monoid_algebra k G) W))
+variables [group G] [comm_ring k] {V W : Type u₃}
+  [add_comm_group V] [module k V] [module (monoid_algebra k G) V]
+  [is_scalar_tower k (monoid_algebra k G) V]
+  [add_comm_group W] [module k W] [module (monoid_algebra k G) W]
+  [is_scalar_tower k (monoid_algebra k G) W]
+  (f : V →ₗ[k] W)
   (h : ∀ (g : G) (v : V), f (single g (1 : k) • v : V) = (single g (1 : k) • (f v) : W))
 include h
 
+-- TODO generalise from groups `G` to monoids??
 /-- Build a `k[G]`-linear map from a `k`-linear map and evidence that it is `G`-equivariant. -/
 def equivariant_of_linear_of_comm : V →ₗ[monoid_algebra k G] W :=
 { to_fun := f,
@@ -410,10 +413,10 @@ def equivariant_of_linear_of_comm : V →ₗ[monoid_algebra k G] W :=
   apply finsupp.induction c,
   { simp, },
   { intros g r c' nm nz w,
-    rw [add_smul, linear_map.map_add, w, add_smul, add_left_inj,
-      single_eq_algebra_map_mul_of, ←smul_smul, ←smul_smul],
-    erw [f.map_smul, h g v],
-    refl, }
+    simp only [add_smul, f.map_add, w, add_left_inj, single_eq_algebra_map_mul_of, ← smul_smul],
+    erw [algebra_map_smul (monoid_algebra k G) r, algebra_map_smul (monoid_algebra k G) r,
+      f.map_smul, h g v, of_apply],
+    all_goals { apply_instance } }
   end, }
 
 @[simp]

src/algebra/monoid_algebra.lean

@@ -2488,11 +2488,12 @@ respectively by `𝕜'` and `𝕜` where `𝕜'` is a normed algebra over `𝕜`
 -/
 
 variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
-{𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
-{E : Type*} [normed_group E] [normed_space 𝕜' E]
-{F : Type*} [normed_group F] [normed_space 𝕜' F]
-{f : semimodule.restrict_scalars 𝕜 𝕜' E → semimodule.restrict_scalars 𝕜 𝕜' F}
-{f' : semimodule.restrict_scalars 𝕜 𝕜' E →L[𝕜'] semimodule.restrict_scalars 𝕜 𝕜' F} {s : set E} {x : E}
+variables {𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
+variables {E : Type*} [normed_group E] [normed_space 𝕜 E] [normed_space 𝕜' E]
+variables [is_scalar_tower 𝕜 𝕜' E]
+variables {F : Type*} [normed_group F] [normed_space 𝕜 F] [normed_space 𝕜' F]
+variables [is_scalar_tower 𝕜 𝕜' F]
+variables {f : E → F} {f' : E →L[𝕜'] F} {s : set E} {x : E}
 
 lemma has_strict_fderiv_at.restrict_scalars (h : has_strict_fderiv_at f f' x) :
   has_strict_fderiv_at f (f'.restrict_scalars 𝕜) x := h
@@ -2532,12 +2533,12 @@ by a normed algebra `𝕜'` over `𝕜`.
 section smul_algebra
 
 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
-{𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
-{E : Type*} [normed_group E] [normed_space 𝕜 E]
-{F : Type*} [normed_group F] [normed_space 𝕜' F]
-{f : E → semimodule.restrict_scalars 𝕜 𝕜' F}
-{f' : E →L[𝕜] semimodule.restrict_scalars 𝕜 𝕜' F} {s : set E} {x : E}
-{c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'} {L : filter E}
+variables {𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
+variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
+variables {F : Type*} [normed_group F] [normed_space 𝕜 F] [normed_space 𝕜' F]
+variables [is_scalar_tower 𝕜 𝕜' F]
+variables {f : E → F} {f' : E →L[𝕜] F} {s : set E} {x : E}
+variables {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'} {L : filter E}
 
 theorem has_strict_fderiv_at.smul_algebra (hc : has_strict_fderiv_at c c' x)
   (hf : has_strict_fderiv_at f f' x) :
@@ -2586,60 +2587,58 @@ lemma fderiv_smul_algebra (hc : differentiable_at 𝕜 c x) (hf : differentiable
 (hc.has_fderiv_at.smul_algebra hf.has_fderiv_at).fderiv
 
 theorem has_strict_fderiv_at.smul_algebra_const
-  (hc : has_strict_fderiv_at c c' x) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : has_strict_fderiv_at c c' x) (f : F) :
   has_strict_fderiv_at (λ y, c y • f) (c'.smul_algebra_right f) x :=
 by simpa only [smul_zero, zero_add] using hc.smul_algebra (has_strict_fderiv_at_const f x)
 
 theorem has_fderiv_within_at.smul_algebra_const
-  (hc : has_fderiv_within_at c c' s x) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : has_fderiv_within_at c c' s x) (f : F) :
   has_fderiv_within_at (λ y, c y • f) (c'.smul_algebra_right f) s x :=
 by simpa only [smul_zero, zero_add] using hc.smul_algebra (has_fderiv_within_at_const f x s)
 
 theorem has_fderiv_at.smul_algebra_const
-  (hc : has_fderiv_at c c' x) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : has_fderiv_at c c' x) (f : F) :
   has_fderiv_at (λ y, c y • f) (c'.smul_algebra_right f) x :=
 by simpa only [smul_zero, zero_add] using hc.smul_algebra (has_fderiv_at_const f x)
 
 lemma differentiable_within_at.smul_algebra_const
-  (hc : differentiable_within_at 𝕜 c s x) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : differentiable_within_at 𝕜 c s x) (f : F) :
   differentiable_within_at 𝕜 (λ y, c y • f) s x :=
 (hc.has_fderiv_within_at.smul_algebra_const f).differentiable_within_at
 
 lemma differentiable_at.smul_algebra_const
-  (hc : differentiable_at 𝕜 c x) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : differentiable_at 𝕜 c x) (f : F) :
   differentiable_at 𝕜 (λ y, c y • f) x :=
 (hc.has_fderiv_at.smul_algebra_const f).differentiable_at
 
 lemma differentiable_on.smul_algebra_const
-  (hc : differentiable_on 𝕜 c s) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : differentiable_on 𝕜 c s) (f : F) :
   differentiable_on 𝕜 (λ y, c y • f) s :=
 λx hx, (hc x hx).smul_algebra_const f
 
 lemma differentiable.smul_algebra_const
-  (hc : differentiable 𝕜 c) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : differentiable 𝕜 c) (f : F) :
   differentiable 𝕜 (λ y, c y • f) :=
 λx, (hc x).smul_algebra_const f
 
 lemma fderiv_within_smul_algebra_const (hxs : unique_diff_within_at 𝕜 s x)
-  (hc : differentiable_within_at 𝕜 c s x) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : differentiable_within_at 𝕜 c s x) (f : F) :
   fderiv_within 𝕜 (λ y, c y • f) s x =
     (fderiv_within 𝕜 c s x).smul_algebra_right f :=
 (hc.has_fderiv_within_at.smul_algebra_const f).fderiv_within hxs
 
 lemma fderiv_smul_algebra_const
-  (hc : differentiable_at 𝕜 c x) (f : semimodule.restrict_scalars 𝕜 𝕜' F) :
+  (hc : differentiable_at 𝕜 c x) (f : F) :
   fderiv 𝕜 (λ y, c y • f) x = (fderiv 𝕜 c x).smul_algebra_right f :=
 (hc.has_fderiv_at.smul_algebra_const f).fderiv
 
 theorem has_strict_fderiv_at.const_smul_algebra (h : has_strict_fderiv_at f f' x) (c : 𝕜') :
   has_strict_fderiv_at (λ x, c • f x) (c • f') x :=
-(c • (1 : (semimodule.restrict_scalars 𝕜 𝕜' F) →L[𝕜] ((semimodule.restrict_scalars 𝕜 𝕜' F))))
-  .has_strict_fderiv_at.comp x h
+(c • (1 : F →L[𝕜] F)).has_strict_fderiv_at.comp x h
 
 theorem has_fderiv_at_filter.const_smul_algebra (h : has_fderiv_at_filter f f' x L) (c : 𝕜') :
   has_fderiv_at_filter (λ x, c • f x) (c • f') x L :=
-(c • (1 : (semimodule.restrict_scalars 𝕜 𝕜' F) →L[𝕜] ((semimodule.restrict_scalars 𝕜 𝕜' F))))
-  .has_fderiv_at_filter.comp x h
+(c • (1 : F →L[𝕜] F)).has_fderiv_at_filter.comp x h
 
 theorem has_fderiv_within_at.const_smul_algebra (h : has_fderiv_within_at f f' s x) (c : 𝕜') :
   has_fderiv_within_at (λ x, c • f x) (c • f') s x :=

src/analysis/calculus/fderiv.lean

@@ -74,7 +74,7 @@ attribute [instance, priority 900] complex.finite_dimensional.proper
 /-- A complex normed vector space is also a real normed vector space. -/
 @[priority 900]
 instance normed_space.restrict_scalars_real (E : Type*) [normed_group E] [normed_space ℂ E] :
-  normed_space ℝ E := normed_space.restrict_scalars' ℝ ℂ E
+  normed_space ℝ E := normed_space.restrict_scalars ℝ ℂ E
 
 /-- The space of continuous linear maps over `ℝ`, from a real vector space to a complex vector
 space, is a normed vector space over `ℂ`. -/

src/analysis/complex/basic.lean

@@ -1127,27 +1127,30 @@ section restrict_scalars
 variables (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
 (E : Type*) [normed_group E] [normed_space 𝕜' E]
 
-/-- `𝕜`-normed space structure induced by a `𝕜'`-normed space structure when `𝕜'` is a
+/-- Warning: This declaration should be used judiciously.
+Please consider using `is_scalar_tower` instead.
+
+`𝕜`-normed space structure induced by a `𝕜'`-normed space structure when `𝕜'` is a
 normed algebra over `𝕜`. Not registered as an instance as `𝕜'` can not be inferred.
 
 The type synonym `semimodule.restrict_scalars 𝕜 𝕜' E` will be endowed with this instance by default.
 -/
-def normed_space.restrict_scalars' : normed_space 𝕜 E :=
+def normed_space.restrict_scalars : normed_space 𝕜 E :=
 { norm_smul_le := λc x, le_of_eq $ begin
     change ∥(algebra_map 𝕜 𝕜' c) • x∥ = ∥c∥ * ∥x∥,
     simp [norm_smul]
   end,
-  ..semimodule.restrict_scalars' 𝕜 𝕜' E }
+  ..restrict_scalars.semimodule 𝕜 𝕜' E }
 
 instance {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [I : normed_group E] :
-  normed_group (semimodule.restrict_scalars 𝕜 𝕜' E) := I
+  normed_group (restrict_scalars 𝕜 𝕜' E) := I
 
 instance semimodule.restrict_scalars.normed_space_orig {𝕜 : Type*} {𝕜' : Type*} {E : Type*}
   [normed_field 𝕜'] [normed_group E] [I : normed_space 𝕜' E] :
-  normed_space 𝕜' (semimodule.restrict_scalars 𝕜 𝕜' E) := I
+  normed_space 𝕜' (restrict_scalars 𝕜 𝕜' E) := I
 
-instance : normed_space 𝕜 (semimodule.restrict_scalars 𝕜 𝕜' E) :=
-(normed_space.restrict_scalars' 𝕜 𝕜' E : normed_space 𝕜 E)
+instance : normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E) :=
+(normed_space.restrict_scalars 𝕜 𝕜' E : normed_space 𝕜 E)
 
 end restrict_scalars
 

src/analysis/normed_space/basic.lean

@@ -280,8 +280,9 @@ lemma is_bounded_bilinear_map_smul :
   bound      := ⟨1, zero_lt_one, λx y, by simp [norm_smul]⟩ }
 
 lemma is_bounded_bilinear_map_smul_algebra {𝕜' : Type*} [normed_field 𝕜']
-  [normed_algebra 𝕜 𝕜'] {E : Type*} [normed_group E] [normed_space 𝕜' E] :
-  is_bounded_bilinear_map 𝕜 (λ (p : 𝕜' × (semimodule.restrict_scalars 𝕜 𝕜' E)), p.1 • p.2) :=
+  [normed_algebra 𝕜 𝕜'] {E : Type*} [normed_group E] [normed_space 𝕜 E] [normed_space 𝕜' E]
+  [is_scalar_tower 𝕜 𝕜' E] :
+  is_bounded_bilinear_map 𝕜 (λ (p : 𝕜' × E), p.1 • p.2) :=
 { add_left   := add_smul,
   smul_left  := λ c x y, by simp [smul_assoc],
   add_right  := smul_add,

src/analysis/normed_space/bounded_linear_maps.lean

@@ -90,14 +90,17 @@ end real
 section complex
 variables {F : Type*} [normed_group F] [normed_space ℂ F]
 
+-- TODO: generalize away from `ℝ` and `ℂ`
+
 -- Inlining the following two definitions causes a type mismatch between
 -- subspace ℝ (semimodule.restrict_scalars ℝ ℂ F) and subspace ℂ F.
 /-- Restrict a `ℂ`-subspace to an `ℝ`-subspace. -/
-noncomputable def restrict_scalars (p : subspace ℂ F) : subspace ℝ F := p.restrict_scalars ℝ
+noncomputable def subspace.restrict_scalars (p : subspace ℂ F) :
+  subspace ℝ F := p.restrict_scalars ℝ
 
 private lemma apply_real (p : subspace ℂ F) (f' : p →L[ℝ] ℝ) :
-  ∃ g : F →L[ℝ] ℝ, (∀ x : restrict_scalars p, g x = f' x) ∧ ∥g∥ = ∥f'∥ :=
-  exists_extension_norm_eq (p.restrict_scalars ℝ) f'
+  ∃ g : F →L[ℝ] ℝ, (∀ x : p.restrict_scalars, g x = f' x) ∧ ∥g∥ = ∥f'∥ :=
+  exists_extension_norm_eq (submodule.restrict_scalars ℝ p) f'
 
 open complex
 

src/analysis/normed_space/hahn_banach.lean

@@ -1111,7 +1111,7 @@ def inner_product_space.is_R_or_C_to_real : inner_product_space ℝ E :=
     simp [this, inner_smul_left, smul_coe_mul_ax],
   end,
   ..has_inner.is_R_or_C_to_real 𝕜,
-  ..normed_space.restrict_scalars' ℝ 𝕜 E }
+  ..normed_space.restrict_scalars ℝ 𝕜 E }
 
 omit 𝕜
 
@@ -1353,7 +1353,9 @@ theorem exists_norm_eq_infi_of_complete_subspace (K : subspace 𝕜 E)
   (h : is_complete (↑K : set E)) : ∀ u : E, ∃ v ∈ K, ∥u - v∥ = ⨅ w : (K : set E), ∥u - w∥ :=
 begin
   letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜,
-  let K' : subspace ℝ E := K.restrict_scalars ℝ,
+  letI : module ℝ E := restrict_scalars.semimodule ℝ 𝕜 E,
+  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
+  let K' : subspace ℝ E := submodule.restrict_scalars ℝ K,
   exact exists_norm_eq_infi_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex
 end
 
@@ -1410,6 +1412,8 @@ theorem norm_eq_infi_iff_inner_eq_zero (K : subspace 𝕜 E) {u : E} {v : E}
   (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set E), ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w⟫ = 0 :=
 begin
   letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜,
+  letI : module ℝ E := restrict_scalars.semimodule ℝ 𝕜 E,
+  letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
   let K' : subspace ℝ E := K.restrict_scalars ℝ,
   split,
   { assume H,

src/analysis/normed_space/inner_product.lean

@@ -708,19 +708,20 @@ section restrict_scalars
 
 variable (𝕜)
 variables {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
-{E' : Type*} [normed_group E'] [normed_space 𝕜' E']
-{F' : Type*} [normed_group F'] [normed_space 𝕜' F']
+variables {E' : Type*} [normed_group E'] [normed_space 𝕜 E'] [normed_space 𝕜' E']
+variables [is_scalar_tower 𝕜 𝕜' E']
+variables {F' : Type*} [normed_group F'] [normed_space 𝕜 F'] [normed_space 𝕜' F']
+variables [is_scalar_tower 𝕜 𝕜' F']
 
 /-- `𝕜`-linear continuous function induced by a `𝕜'`-linear continuous function when `𝕜'` is a
 normed algebra over `𝕜`. -/
 def restrict_scalars (f : E' →L[𝕜'] F') :
-  (semimodule.restrict_scalars 𝕜 𝕜' E') →L[𝕜] (semimodule.restrict_scalars 𝕜 𝕜' F') :=
+  E' →L[𝕜] F' :=
 { cont := f.cont,
   ..linear_map.restrict_scalars 𝕜 (f.to_linear_map) }
 
 @[simp, norm_cast] lemma restrict_scalars_coe_eq_coe (f : E' →L[𝕜'] F') :
-  (f.restrict_scalars 𝕜 :
-    (semimodule.restrict_scalars 𝕜 𝕜' E') →ₗ[𝕜] (semimodule.restrict_scalars 𝕜 𝕜' F')) =
+  (f.restrict_scalars 𝕜 : E' →ₗ[𝕜] F') =
   (f : E' →ₗ[𝕜'] F').restrict_scalars 𝕜 := rfl
 
 @[simp, norm_cast squash] lemma restrict_scalars_coe_eq_coe' (f : E' →L[𝕜'] F') :
@@ -731,9 +732,10 @@ end restrict_scalars
 section extend_scalars
 
 variables {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
-{F' : Type*} [normed_group F'] [normed_space 𝕜' F']
+variables {F' : Type*} [normed_group F'] [normed_space 𝕜 F'] [normed_space 𝕜' F']
+variables [is_scalar_tower 𝕜 𝕜' F']
 
-instance has_scalar_extend_scalars : has_scalar 𝕜' (E →L[𝕜] (semimodule.restrict_scalars 𝕜 𝕜' F')) :=
+instance has_scalar_extend_scalars : has_scalar 𝕜' (E →L[𝕜] F') :=
 { smul := λ c f, (c • f.to_linear_map).mk_continuous (∥c∥ * ∥f∥)
 begin
   assume x,
@@ -742,27 +744,24 @@ begin
   ... = ∥c∥ * ∥f∥ * ∥x∥ : (mul_assoc _ _ _).symm
 end }
 
-instance module_extend_scalars : module 𝕜' (E →L[𝕜] (semimodule.restrict_scalars 𝕜 𝕜' F')) :=
+instance module_extend_scalars : module 𝕜' (E →L[𝕜] F') :=
 { smul_zero := λ _, ext $ λ _, smul_zero _,
   zero_smul := λ _, ext $ λ _, zero_smul _ _,
   one_smul  := λ _, ext $ λ _, one_smul _ _,
   mul_smul  := λ _ _ _, ext $ λ _, mul_smul _ _ _,
   add_smul  := λ _ _ _, ext $ λ _, add_smul _ _ _,
   smul_add  := λ _ _ _, ext $ λ _, smul_add _ _ _ }
 
-instance normed_space_extend_scalars : normed_space 𝕜' (E →L[𝕜] (semimodule.restrict_scalars 𝕜 𝕜' F')) :=
+instance normed_space_extend_scalars : normed_space 𝕜' (E →L[𝕜] F') :=
 { norm_smul_le := λ c f,
     linear_map.mk_continuous_norm_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _ }
 
 /-- When `f` is a continuous linear map taking values in `S`, then `λb, f b • x` is a
 continuous linear map. -/
-def smul_algebra_right (f : E →L[𝕜] 𝕜') (x : semimodule.restrict_scalars 𝕜 𝕜' F') :
-  E →L[𝕜] (semimodule.restrict_scalars 𝕜 𝕜' F') :=
-{ cont := by continuity!,
-  .. smul_algebra_right f.to_linear_map x }
+def smul_algebra_right (f : E →L[𝕜] 𝕜') (x : F') : E →L[𝕜] F' :=
+{ cont := by continuity!, .. f.to_linear_map.smul_algebra_right x }
 
-@[simp] theorem smul_algebra_right_apply
-  (f : E →L[𝕜] 𝕜') (x : semimodule.restrict_scalars 𝕜 𝕜' F') (c : E) :
+@[simp] theorem smul_algebra_right_apply (f : E →L[𝕜] 𝕜') (x : F') (c : E) :
   smul_algebra_right f x c = f c • x := rfl
 
 end extend_scalars

src/analysis/normed_space/operator_norm.lean

@@ -362,6 +362,8 @@ by rw [← of_real_rat_cast, of_real_im]
 
 /-! ### Characteristic zero -/
 
+-- TODO: I think this can be instance, because it is a `Prop`
+
 /--
 ℝ and ℂ are both of characteristic zero.