refactor(linear_algebra,algebra/algebra): generalize linear_map.smul_right (#5967)

* the new `linear_map.smul_right` generalizes both the old
  `linear_map.smul_right` and the old `linear_map.smul_algebra_right`;
* add `smul_comm_class` for `linear_map`s.

Author: urkud

src/algebra/algebra/basic.lean

@@ -1366,10 +1366,6 @@ end semimodule
 end restrict_scalars
 
 namespace linear_map
-section extend_scalars
-/-! When `V` is an `R`-module and `W` is an `S`-module, where `S` is an algebra over `R`, then
-the collection of `R`-linear maps from `V` to `W` admits an `S`-module structure, given by
-multiplication in the target. -/
 
 variables (R : Type*) [comm_semiring R] (S : Type*) [semiring S] [algebra R S]
   (V : Type*) [add_comm_monoid V] [semimodule R V]
@@ -1379,16 +1375,4 @@ instance is_scalar_tower_extend_scalars :
   is_scalar_tower R S (V →ₗ[R] W) :=
 { smul_assoc := λ r s f, by simp only [(•), coe_mk, smul_assoc] }
 
-variables {R S V W}
-
-/-- When `f` is a linear map taking values in `S`, then `λb, f b • x` is a linear map. -/
-def smul_algebra_right (f : V →ₗ[R] S) (x : W) : V →ₗ[R] W :=
-{ to_fun := λb, f b • x,
-  map_add' := by simp [add_smul],
-  map_smul' := λ b y, by { simp [algebra.smul_def, ← smul_smul], } }
-
-@[simp] theorem smul_algebra_right_apply (f : V →ₗ[R] S) (x : W) (c : V) :
-  smul_algebra_right f x c = f c • x := rfl
-
-end extend_scalars
 end linear_map

src/analysis/normed_space/operator_norm.lean

@@ -764,7 +764,7 @@ instance normed_space_extend_scalars : normed_space 𝕜' (E →L[𝕜] F') :=
 /-- 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 : F') : E →L[𝕜] F' :=
-{ cont := by continuity!, .. f.to_linear_map.smul_algebra_right x }
+{ cont := by continuity!, .. f.to_linear_map.smul_right x }
 
 @[simp] theorem smul_algebra_right_apply (f : E →L[𝕜] 𝕜') (x : F') (c : E) :
   smul_algebra_right f x c = f c • x := rfl

src/linear_algebra/basic.lean

@@ -187,12 +187,20 @@ lemma sum_apply (t : finset ι) (f : ι → M →ₗ[R] M₂) (b : M) :
   (∑ d in t, f d) b = ∑ d in t, f d b :=
 (t.sum_hom (λ g : M →ₗ[R] M₂, g b)).symm
 
-/-- `λb, f b • x` is a linear map. -/
-def smul_right (f : M₂ →ₗ[R] R) (x : M) : M₂ →ₗ[R] M :=
-⟨λb, f b • x, by simp [add_smul], by simp [smul_smul]⟩.
+section smul_right
 
-@[simp] theorem smul_right_apply (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
-  (smul_right f x : M₂ → M) c = f c • x := rfl
+variables {S : Type*} [semiring S] [semimodule R S] [semimodule S M] [is_scalar_tower R S M]
+
+/-- When `f` is an `R`-linear map taking values in `S`, then `λb, f b • x` is an `R`-linear map. -/
+def smul_right (f : M₂ →ₗ[R] S) (x : M) : M₂ →ₗ[R] M :=
+{ to_fun := λb, f b • x,
+  map_add' := λ x y, by rw [f.map_add, add_smul],
+  map_smul' := λ b y, by rw [f.map_smul, smul_assoc] }
+
+@[simp] theorem smul_right_apply (f : M₂ →ₗ[R] S) (x : M) (c : M₂) :
+  smul_right f x c = f c • x := rfl
+
+end smul_right
 
 instance : has_one (M →ₗ[R] M) := ⟨linear_map.id⟩
 instance : has_mul (M →ₗ[R] M) := ⟨linear_map.comp⟩
@@ -373,6 +381,11 @@ instance : has_scalar S (M →ₗ[R] M₂) :=
 
 @[simp] lemma smul_apply (a : S) (x : M) : (a • f) x = a • f x := rfl
 
+instance {T : Type*} [monoid T] [distrib_mul_action T M₂] [smul_comm_class R T M₂]
+  [smul_comm_class S T M₂] :
+  smul_comm_class S T (M →ₗ[R] M₂) :=
+⟨λ a b f, ext $ λ x, smul_comm _ _ _⟩
+
 instance : distrib_mul_action S (M →ₗ[R] M₂) :=
 { one_smul := λ f, ext $ λ _, one_smul _ _,
   mul_smul := λ c c' f, ext $ λ _, mul_smul _ _ _,

src/linear_algebra/finsupp.lean

@@ -380,7 +380,7 @@ variables (α) {α' : Type*} (M) {M' : Type*} (R)
 
 /-- Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and
     evaluates this linear combination. -/
-protected def total : (α →₀ R) →ₗ M := finsupp.lsum (λ i, linear_map.id.smul_right (v i))
+protected def total : (α →₀ R) →ₗ[R] M := finsupp.lsum (λ i, linear_map.id.smul_right (v i))
 
 variables {α M v}