chore(analysis/normed_space/operator_norm): fix naming of continuous_linear_map.lmul and similar (#15968)

This renames the continuous linear (bilinear) map given by multiplication in a non-unital algebra to match the non-continuous version (`linear_map.mul`). The changes are as follows:

1. `continuous_linear_map.lmul` → `continuous_linear_map.mul` (the "l" was for "linear", which is redundant)
2. `continuous_linear_map.lmul_right` is deleted. This is literally just the `continuous_linear_map.flip` of the map in (1) above. It's only use in mathlib is to define the map in (3) below, and creating it as a separate def seems unnecessary (and actively obscures the `.flip`)
3. `continuous_linear_map.lmul_left_right` → `continuous_linear_map.mul_left_right`. This matches `linear_map.mul_left_right` (although the latter is uncurried).

Docstrings have also been updated, both to reflect the non-unital generalization from #15868, but also because the old docstrings mentioned "left multiplication", but this should just be called "multiplication".

Author: j-loreaux

src/analysis/calculus/cont_diff.lean

@@ -2582,7 +2582,7 @@ variables {𝔸 𝔸' ι 𝕜' : Type*} [normed_ring 𝔸] [normed_algebra 𝕜
 
 /- The product is smooth. -/
 lemma cont_diff_mul : cont_diff 𝕜 n (λ p : 𝔸 × 𝔸, p.1 * p.2) :=
-(continuous_linear_map.lmul 𝕜 𝔸).is_bounded_bilinear_map.cont_diff
+(continuous_linear_map.mul 𝕜 𝔸).is_bounded_bilinear_map.cont_diff
 
 /-- The product of two `C^n` functions within a set at a point is `C^n` within this set
 at this point. -/
@@ -2881,12 +2881,12 @@ begin
         exact (inverse_continuous_at x').continuous_within_at },
       { simp [ftaylor_series_within] } } },
   { apply cont_diff_at_succ_iff_has_fderiv_at.mpr,
-    refine ⟨λ (x : R), - lmul_left_right 𝕜 R (inverse x) (inverse x), _, _⟩,
+    refine ⟨λ (x : R), - mul_left_right 𝕜 R (inverse x) (inverse x), _, _⟩,
     { refine ⟨{y : R | is_unit y}, x.nhds, _⟩,
       rintros _ ⟨y, rfl⟩,
       rw [inverse_unit],
       exact has_fderiv_at_ring_inverse y },
-    { convert (lmul_left_right_is_bounded_bilinear 𝕜 R).cont_diff.neg.comp_cont_diff_at
+    { convert (mul_left_right_is_bounded_bilinear 𝕜 R).cont_diff.neg.comp_cont_diff_at
         (x : R) (IH.prod IH) } },
   { exact cont_diff_at_top.mpr Itop }
 end

src/analysis/calculus/fderiv.lean

@@ -2371,7 +2371,7 @@ variables {𝔸 𝔸' : Type*} [normed_ring 𝔸] [normed_comm_ring 𝔸'] [norm
 theorem has_strict_fderiv_at.mul' {x : E} (ha : has_strict_fderiv_at a a' x)
   (hb : has_strict_fderiv_at b b' x) :
   has_strict_fderiv_at (λ y, a y * b y) (a x • b' + a'.smul_right (b x)) x :=
-((continuous_linear_map.lmul 𝕜 𝔸).is_bounded_bilinear_map.has_strict_fderiv_at (a x, b x)).comp x
+((continuous_linear_map.mul 𝕜 𝔸).is_bounded_bilinear_map.has_strict_fderiv_at (a x, b x)).comp x
   (ha.prod hb)
 
 theorem has_strict_fderiv_at.mul
@@ -2382,7 +2382,7 @@ by { convert hc.mul' hd, ext z, apply mul_comm }
 theorem has_fderiv_within_at.mul'
   (ha : has_fderiv_within_at a a' s x) (hb : has_fderiv_within_at b b' s x) :
   has_fderiv_within_at (λ y, a y * b y) (a x • b' + a'.smul_right (b x)) s x :=
-((continuous_linear_map.lmul 𝕜 𝔸).is_bounded_bilinear_map.has_fderiv_at
+((continuous_linear_map.mul 𝕜 𝔸).is_bounded_bilinear_map.has_fderiv_at
   (a x, b x)).comp_has_fderiv_within_at x (ha.prod hb)
 
 theorem has_fderiv_within_at.mul
@@ -2393,7 +2393,7 @@ by { convert hc.mul' hd, ext z, apply mul_comm }
 theorem has_fderiv_at.mul'
   (ha : has_fderiv_at a a' x) (hb : has_fderiv_at b b' x) :
   has_fderiv_at (λ y, a y * b y) (a x • b' + a'.smul_right (b x)) x :=
-((continuous_linear_map.lmul 𝕜 𝔸).is_bounded_bilinear_map.has_fderiv_at (a x, b x)).comp x
+((continuous_linear_map.mul 𝕜 𝔸).is_bounded_bilinear_map.has_fderiv_at (a x, b x)).comp x
   (ha.prod hb)
 
 theorem has_fderiv_at.mul (hc : has_fderiv_at c c' x) (hd : has_fderiv_at d d' x) :
@@ -2458,23 +2458,23 @@ lemma fderiv_mul (hc : differentiable_at 𝕜 c x) (hd : differentiable_at 𝕜
 
 theorem has_strict_fderiv_at.mul_const' (ha : has_strict_fderiv_at a a' x) (b : 𝔸) :
   has_strict_fderiv_at (λ y, a y * b) (a'.smul_right b) x :=
-(((continuous_linear_map.lmul 𝕜 𝔸).flip b).has_strict_fderiv_at).comp x ha
+(((continuous_linear_map.mul 𝕜 𝔸).flip b).has_strict_fderiv_at).comp x ha
 
 theorem has_strict_fderiv_at.mul_const (hc : has_strict_fderiv_at c c' x) (d : 𝔸') :
   has_strict_fderiv_at (λ y, c y * d) (d • c') x :=
 by { convert hc.mul_const' d, ext z, apply mul_comm }
 
 theorem has_fderiv_within_at.mul_const' (ha : has_fderiv_within_at a a' s x) (b : 𝔸) :
   has_fderiv_within_at (λ y, a y * b) (a'.smul_right b) s x :=
-(((continuous_linear_map.lmul 𝕜 𝔸).flip b).has_fderiv_at).comp_has_fderiv_within_at x ha
+(((continuous_linear_map.mul 𝕜 𝔸).flip b).has_fderiv_at).comp_has_fderiv_within_at x ha
 
 theorem has_fderiv_within_at.mul_const (hc : has_fderiv_within_at c c' s x) (d : 𝔸') :
   has_fderiv_within_at (λ y, c y * d) (d • c') s x :=
 by { convert hc.mul_const' d, ext z, apply mul_comm }
 
 theorem has_fderiv_at.mul_const' (ha : has_fderiv_at a a' x) (b : 𝔸) :
   has_fderiv_at (λ y, a y * b) (a'.smul_right b) x :=
-(((continuous_linear_map.lmul 𝕜 𝔸).flip b).has_fderiv_at).comp x ha
+(((continuous_linear_map.mul 𝕜 𝔸).flip b).has_fderiv_at).comp x ha
 
 theorem has_fderiv_at.mul_const (hc : has_fderiv_at c c' x) (d : 𝔸') :
   has_fderiv_at (λ y, c y * d) (d • c') x :=
@@ -2517,16 +2517,16 @@ lemma fderiv_mul_const (hc : differentiable_at 𝕜 c x) (d : 𝔸') :
 
 theorem has_strict_fderiv_at.const_mul (ha : has_strict_fderiv_at a a' x) (b : 𝔸) :
   has_strict_fderiv_at (λ y, b * a y) (b • a') x :=
-(((continuous_linear_map.lmul 𝕜 𝔸) b).has_strict_fderiv_at).comp x ha
+(((continuous_linear_map.mul 𝕜 𝔸) b).has_strict_fderiv_at).comp x ha
 
 theorem has_fderiv_within_at.const_mul
   (ha : has_fderiv_within_at a a' s x) (b : 𝔸) :
   has_fderiv_within_at (λ y, b * a y) (b • a') s x :=
-(((continuous_linear_map.lmul 𝕜 𝔸) b).has_fderiv_at).comp_has_fderiv_within_at x ha
+(((continuous_linear_map.mul 𝕜 𝔸) b).has_fderiv_at).comp_has_fderiv_within_at x ha
 
 theorem has_fderiv_at.const_mul (ha : has_fderiv_at a a' x) (b : 𝔸) :
   has_fderiv_at (λ y, b * a y) (b • a') x :=
-(((continuous_linear_map.lmul 𝕜 𝔸) b).has_fderiv_at).comp x ha
+(((continuous_linear_map.mul 𝕜 𝔸) b).has_fderiv_at).comp x ha
 
 lemma differentiable_within_at.const_mul
   (ha : differentiable_within_at 𝕜 a s x) (b : 𝔸) :
@@ -2563,7 +2563,7 @@ open normed_ring continuous_linear_map ring
 /-- At an invertible element `x` of a normed algebra `R`, the Fréchet derivative of the inversion
 operation is the linear map `λ t, - x⁻¹ * t * x⁻¹`. -/
 lemma has_fderiv_at_ring_inverse (x : Rˣ) :
-  has_fderiv_at ring.inverse (-lmul_left_right 𝕜 R ↑x⁻¹ ↑x⁻¹) x :=
+  has_fderiv_at ring.inverse (-mul_left_right 𝕜 R ↑x⁻¹ ↑x⁻¹) x :=
 begin
   have h_is_o : (λ (t : R), inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] (λ (t : R), t),
   { refine (inverse_add_norm_diff_second_order x).trans_is_o ((is_o_norm_norm).mp _),
@@ -2577,15 +2577,15 @@ begin
   simp only [has_fderiv_at, has_fderiv_at_filter],
   convert h_is_o.comp_tendsto h_lim,
   ext y,
-  simp only [coe_comp', function.comp_app, lmul_left_right_apply, neg_apply, inverse_unit x,
+  simp only [coe_comp', function.comp_app, mul_left_right_apply, neg_apply, inverse_unit x,
     units.inv_mul, add_sub_cancel'_right, mul_sub, sub_mul, one_mul, sub_neg_eq_add]
 end
 
 lemma differentiable_at_inverse (x : Rˣ) : differentiable_at 𝕜 (@ring.inverse R _) x :=
 (has_fderiv_at_ring_inverse x).differentiable_at
 
 lemma fderiv_inverse (x : Rˣ) :
-  fderiv 𝕜 (@ring.inverse R _) x = - lmul_left_right 𝕜 R ↑x⁻¹ ↑x⁻¹ :=
+  fderiv 𝕜 (@ring.inverse R _) x = - mul_left_right 𝕜 R ↑x⁻¹ ↑x⁻¹ :=
 (has_fderiv_at_ring_inverse x).fderiv
 
 end algebra_inverse

src/analysis/convolution.lean

@@ -18,7 +18,7 @@ group as domain. We use a continuous bilinear operation `L` on these function va
 "multiplication". The domain must be equipped with a Haar measure `μ`
 (though many individual results have weaker conditions on `μ`).
 
-For many applications we can take `L = lsmul ℝ ℝ` or `L = lmul ℝ ℝ`.
+For many applications we can take `L = lsmul ℝ ℝ` or `L = mul ℝ ℝ`.
 
 We also define `convolution_exists` and `convolution_exists_at` to state that the convolution is
 well-defined (everywhere or at a single point). These conditions are needed for pointwise
@@ -375,8 +375,8 @@ lemma convolution_lsmul [has_sub G] {f : G → 𝕜} {g : G → F} :
   (f ⋆[lsmul 𝕜 𝕜, μ] g : G → F) x = ∫ t, f t • g (x - t) ∂μ := rfl
 
 /-- The definition of convolution where the bilinear operator is multiplication. -/
-lemma convolution_lmul [has_sub G] [normed_space ℝ 𝕜] [complete_space 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
-  (f ⋆[lmul 𝕜 𝕜, μ] g) x = ∫ t, f t * g (x - t) ∂μ := rfl
+lemma convolution_mul [has_sub G] [normed_space ℝ 𝕜] [complete_space 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
+  (f ⋆[mul 𝕜 𝕜, μ] g) x = ∫ t, f t * g (x - t) ∂μ := rfl
 
 section group
 
@@ -547,8 +547,8 @@ lemma convolution_lsmul_swap {f : G → 𝕜} {g : G → F}:
 convolution_eq_swap _
 
 /-- The symmetric definition of convolution where the bilinear operator is multiplication. -/
-lemma convolution_lmul_swap [normed_space ℝ 𝕜] [complete_space 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
-  (f ⋆[lmul 𝕜 𝕜, μ] g) x = ∫ t, f (x - t) * g t ∂μ :=
+lemma convolution_mul_swap [normed_space ℝ 𝕜] [complete_space 𝕜] {f : G → 𝕜} {g : G → 𝕜} :
+  (f ⋆[mul 𝕜 𝕜, μ] g) x = ∫ t, f (x - t) * g t ∂μ :=
 convolution_eq_swap _
 
 end measurable

src/analysis/normed_space/bounded_linear_maps.lean

@@ -488,11 +488,12 @@ end
 
 variables (𝕜)
 
-/-- The function `lmul_left_right : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜')` is a bounded bilinear map. -/
-lemma continuous_linear_map.lmul_left_right_is_bounded_bilinear
+/-- The function `continuous_linear_map.mul_left_right : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜')` is a bounded
+bilinear map. -/
+lemma continuous_linear_map.mul_left_right_is_bounded_bilinear
   (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
-  is_bounded_bilinear_map 𝕜 (λ p : 𝕜' × 𝕜', continuous_linear_map.lmul_left_right 𝕜 𝕜' p.1 p.2) :=
-(continuous_linear_map.lmul_left_right 𝕜 𝕜').is_bounded_bilinear_map
+  is_bounded_bilinear_map 𝕜 (λ p : 𝕜' × 𝕜', continuous_linear_map.mul_left_right 𝕜 𝕜' p.1 p.2) :=
+(continuous_linear_map.mul_left_right 𝕜 𝕜').is_bounded_bilinear_map
 
 variables {𝕜}
 

src/analysis/normed_space/operator_norm.lean

@@ -828,77 +828,56 @@ section non_unital
 variables (𝕜) (𝕜' : Type*) [non_unital_semi_normed_ring 𝕜'] [normed_space 𝕜 𝕜']
   [is_scalar_tower 𝕜 𝕜' 𝕜'] [smul_comm_class 𝕜 𝕜' 𝕜']
 
-/-- Left multiplication in a normed algebra as a continuous bilinear map. -/
-def lmul : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-(linear_map.mul 𝕜 𝕜').mk_continuous₂ 1 $
+/-- Multiplication in a non-unital normed algebra as a continuous bilinear map. -/
+def mul : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' := (linear_map.mul 𝕜 𝕜').mk_continuous₂ 1 $
   λ x y, by simpa using norm_mul_le x y
 
-@[simp] lemma lmul_apply (x y : 𝕜') : lmul 𝕜 𝕜' x y = x * y := rfl
+@[simp] lemma mul_apply' (x y : 𝕜') : mul 𝕜 𝕜' x y = x * y := rfl
 
-@[simp] lemma op_norm_lmul_apply_le (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ ≤ ∥x∥ :=
+@[simp] lemma op_norm_mul_apply_le (x : 𝕜') : ∥mul 𝕜 𝕜' x∥ ≤ ∥x∥ :=
 (op_norm_le_bound _ (norm_nonneg x) (norm_mul_le x))
 
-/-- Right-multiplication in a normed algebra, considered as a continuous linear map. -/
-def lmul_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' := (lmul 𝕜 𝕜').flip
+/-- 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 `linear_map.mul_left_right`,
+but there is a minor difference: `linear_map.mul_left_right` is uncurried. -/
+def mul_left_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+((compL 𝕜 𝕜' 𝕜' 𝕜').comp (mul 𝕜 𝕜').flip).flip.comp (mul 𝕜 𝕜')
 
-@[simp] lemma lmul_right_apply (x y : 𝕜') : lmul_right 𝕜 𝕜' x y = y * x := rfl
+@[simp] lemma mul_left_right_apply (x y z : 𝕜') :
+  mul_left_right 𝕜 𝕜' x y z = x * z * y := rfl
 
-@[simp] lemma op_norm_lmul_right_apply_le (x : 𝕜') : ∥lmul_right 𝕜 𝕜' x∥ ≤ ∥x∥ :=
-op_norm_le_bound _ (norm_nonneg x) (λ y, (norm_mul_le y x).trans_eq (mul_comm _ _))
-
-/-- Simultaneous left- and right-multiplication in a normed algebra, considered as a continuous
-trilinear map. -/
-def lmul_left_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-((compL 𝕜 𝕜' 𝕜' 𝕜').comp (lmul_right 𝕜 𝕜')).flip.comp (lmul 𝕜 𝕜')
-
-@[simp] lemma lmul_left_right_apply (x y z : 𝕜') :
-  lmul_left_right 𝕜 𝕜' x y z = x * z * y := rfl
-
-lemma op_norm_lmul_left_right_apply_apply_le (x y : 𝕜') :
-  ∥lmul_left_right 𝕜 𝕜' x y∥ ≤ ∥x∥ * ∥y∥ :=
+lemma op_norm_mul_left_right_apply_apply_le (x y : 𝕜') :
+  ∥mul_left_right 𝕜 𝕜' x y∥ ≤ ∥x∥ * ∥y∥ :=
 (op_norm_comp_le _ _).trans $ (mul_comm _ _).trans_le $
-  mul_le_mul (op_norm_lmul_apply_le _ _ _) (op_norm_lmul_right_apply_le _ _ _)
+  mul_le_mul (op_norm_mul_apply_le _ _ _)
+    (op_norm_le_bound _ (norm_nonneg _) (λ _, (norm_mul_le _ _).trans_eq (mul_comm _ _)))
     (norm_nonneg _) (norm_nonneg _)
 
-lemma op_norm_lmul_left_right_apply_le (x : 𝕜') :
-  ∥lmul_left_right 𝕜 𝕜' x∥ ≤ ∥x∥ :=
-op_norm_le_bound _ (norm_nonneg x) (op_norm_lmul_left_right_apply_apply_le 𝕜 𝕜' x)
+lemma op_norm_mul_left_right_apply_le (x : 𝕜') :
+  ∥mul_left_right 𝕜 𝕜' x∥ ≤ ∥x∥ :=
+op_norm_le_bound _ (norm_nonneg x) (op_norm_mul_left_right_apply_apply_le 𝕜 𝕜' x)
 
-lemma op_norm_lmul_left_right_le :
-  ∥lmul_left_right 𝕜 𝕜'∥ ≤ 1 :=
-op_norm_le_bound _ zero_le_one (λ x, (one_mul ∥x∥).symm ▸ op_norm_lmul_left_right_apply_le 𝕜 𝕜' x)
+lemma op_norm_mul_left_right_le :
+  ∥mul_left_right 𝕜 𝕜'∥ ≤ 1 :=
+op_norm_le_bound _ zero_le_one (λ x, (one_mul ∥x∥).symm ▸ op_norm_mul_left_right_apply_le 𝕜 𝕜' x)
 
 end non_unital
 
 section unital
 variables (𝕜) (𝕜' : Type*) [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] [norm_one_class 𝕜']
 
-/-- Left multiplication in a normed algebra as a linear isometry to the space of
+/-- Multiplication in a normed algebra as a linear isometry to the space of
 continuous linear maps. -/
-def lmulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-{ to_linear_map := lmul 𝕜 𝕜',
-  norm_map' := λ x, le_antisymm (op_norm_lmul_apply_le _ _ _)
+def mulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+{ to_linear_map := mul 𝕜 𝕜',
+  norm_map' := λ x, le_antisymm (op_norm_mul_apply_le _ _ _)
     (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [norm_one],
           apply_instance }) }
 
-@[simp] lemma coe_lmulₗᵢ : ⇑(lmulₗᵢ 𝕜 𝕜') = lmul 𝕜 𝕜' := rfl
-
-@[simp] lemma op_norm_lmul_apply (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ = ∥x∥ :=
-(lmulₗᵢ 𝕜 𝕜').norm_map x
-
-@[simp] lemma op_norm_lmul_right_apply (x : 𝕜') : ∥lmul_right 𝕜 𝕜' x∥ = ∥x∥ :=
-le_antisymm
-  (op_norm_lmul_right_apply_le _ _ _)
-  (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [norm_one],
-        apply_instance })
-
-/-- Right-multiplication in a normed algebra, considered as a linear isometry to the space of
-continuous linear maps. -/
-def lmul_rightₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-{ to_linear_map := lmul_right 𝕜 𝕜',
-  norm_map' := op_norm_lmul_right_apply 𝕜 𝕜' }
+@[simp] lemma coe_mulₗᵢ : ⇑(mulₗᵢ 𝕜 𝕜') = mul 𝕜 𝕜' := rfl
 
-@[simp] lemma coe_lmul_rightₗᵢ : ⇑(lmul_rightₗᵢ 𝕜 𝕜') = lmul_right 𝕜 𝕜' := rfl
+@[simp] lemma op_norm_mul_apply (x : 𝕜') : ∥mul 𝕜 𝕜' x∥ = ∥x∥ :=
+(mulₗᵢ 𝕜 𝕜').norm_map x
 
 end unital
 
@@ -1659,11 +1638,9 @@ variables (𝕜) (𝕜' : Type*)
 section
 variables [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
 
-@[simp] lemma op_norm_lmul [norm_one_class 𝕜'] : ∥lmul 𝕜 𝕜'∥ = 1 :=
-by haveI := norm_one_class.nontrivial 𝕜'; exact (lmulₗᵢ 𝕜 𝕜').norm_to_continuous_linear_map
+@[simp] lemma op_norm_mul [norm_one_class 𝕜'] : ∥mul 𝕜 𝕜'∥ = 1 :=
+by haveI := norm_one_class.nontrivial 𝕜'; exact (mulₗᵢ 𝕜 𝕜').norm_to_continuous_linear_map
 
-@[simp] lemma op_norm_lmul_right [norm_one_class 𝕜'] : ∥lmul_right 𝕜 𝕜'∥ = 1 :=
-(op_norm_flip (lmul 𝕜 𝕜')).trans (op_norm_lmul _ _)
 end
 
 /-- The norm of `lsmul` equals 1 in any nontrivial normed group.