feat: generalize ContinuousMultilinearLinearMap.mkPiField to `mkPiR…

…ing` (leanprover-community#9910)

This matches the generality of the non-continuous versions.

The `norm_smulRight` lemma is the only new result.

Mathlib/Analysis/Analytic/Basic.lean

@@ -941,7 +941,7 @@ If a function `f : E → F` has two representations as power series at a point `
 to formal multilinear series `p₁` and `p₂`, then these representations agree term-by-term. That is,
 for any `n : ℕ` and `y : E`, `p₁ n (fun i ↦ y) = p₂ n (fun i ↦ y)`. In the one-dimensional case,
 when `f : 𝕜 → E`, the continuous multilinear maps `p₁ n` and `p₂ n` are given by
-`ContinuousMultilinearMap.mkPiField`, and hence are determined completely by the value of
+`ContinuousMultilinearMap.mkPiRing`, and hence are determined completely by the value of
 `p₁ n (fun i ↦ 1)`, so `p₁ = p₂`. Consequently, the radius of convergence for one series can be
 transferred to the other.
 -/
@@ -1026,7 +1026,7 @@ theorem HasFPowerSeriesAt.eq_zero {p : FormalMultilinearSeries 𝕜 𝕜 E} {x :
   -- porting note: `funext; ext` was `ext (n x)`
   funext n
   ext x
-  rw [← mkPiField_apply_one_eq_self (p n)]
+  rw [← mkPiRing_apply_one_eq_self (p n)]
   -- porting note: nasty hack, was `simp [h.apply_eq_zero n 1]`
   have := Or.intro_right ?_ (h.apply_eq_zero n 1)
   simpa using this

Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

@@ -292,10 +292,10 @@ def coeff (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) : E :=
   p n 1
 #align formal_multilinear_series.coeff FormalMultilinearSeries.coeff
 
-theorem mkPiField_coeff_eq (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) :
-    ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (p.coeff n) = p n :=
-  (p n).mkPiField_apply_one_eq_self
-#align formal_multilinear_series.mk_pi_field_coeff_eq FormalMultilinearSeries.mkPiField_coeff_eq
+theorem mkPiRing_coeff_eq (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) :
+    ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n) = p n :=
+  (p n).mkPiRing_apply_one_eq_self
+#align formal_multilinear_series.mk_pi_field_coeff_eq FormalMultilinearSeries.mkPiRing_coeff_eq
 
 @[simp]
 theorem apply_eq_prod_smul_coeff : p n y = (∏ i, y i) • p.coeff n := by
@@ -305,7 +305,7 @@ theorem apply_eq_prod_smul_coeff : p n y = (∏ i, y i) • p.coeff n := by
 #align formal_multilinear_series.apply_eq_prod_smul_coeff FormalMultilinearSeries.apply_eq_prod_smul_coeff
 
 theorem coeff_eq_zero : p.coeff n = 0 ↔ p n = 0 := by
-  rw [← mkPiField_coeff_eq p, ContinuousMultilinearMap.mkPiField_eq_zero_iff]
+  rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.mkPiRing_eq_zero_iff]
 #align formal_multilinear_series.coeff_eq_zero FormalMultilinearSeries.coeff_eq_zero
 
 @[simp]
@@ -314,7 +314,7 @@ theorem apply_eq_pow_smul_coeff : (p n fun _ => z) = z ^ n • p.coeff n := by s
 
 @[simp]
 theorem norm_apply_eq_norm_coef : ‖p n‖ = ‖coeff p n‖ := by
-  rw [← mkPiField_coeff_eq p, ContinuousMultilinearMap.norm_mkPiField]
+  rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.norm_mkPiRing]
 #align formal_multilinear_series.norm_apply_eq_norm_coef FormalMultilinearSeries.norm_apply_eq_norm_coef
 
 end Coef

Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

@@ -187,7 +187,7 @@ theorem iteratedDerivWithin_succ {x : 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x)
     iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x := by
   rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
     iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_fderivWithin _ hxs, derivWithin]
-  change ((ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) ((fderivWithin 𝕜
+  change ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜
     (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun i : Fin n => 1) =
     (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
   simp

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -916,48 +916,31 @@ theorem norm_mkPiAlgebraFin [NormOneClass A] :
 
 end
 
-variable (𝕜 ι)
-
-/-- The canonical continuous multilinear map on `𝕜^ι`, associating to `m` the product of all the
-`m i` (multiplied by a fixed reference element `z` in the target module) -/
-protected def mkPiField (z : G) : ContinuousMultilinearMap 𝕜 (fun _ : ι => 𝕜) G :=
-  MultilinearMap.mkContinuous (MultilinearMap.mkPiRing 𝕜 ι z) ‖z‖ fun m => by
-    simp only [MultilinearMap.mkPiRing_apply, norm_smul, norm_prod, mul_comm, le_rfl]
-#align continuous_multilinear_map.mk_pi_field ContinuousMultilinearMap.mkPiField
-
-variable {𝕜 ι}
-
 @[simp]
-theorem mkPiField_apply (z : G) (m : ι → 𝕜) :
-    (ContinuousMultilinearMap.mkPiField 𝕜 ι z : (ι → 𝕜) → G) m = (∏ i, m i) • z :=
-  rfl
-#align continuous_multilinear_map.mk_pi_field_apply ContinuousMultilinearMap.mkPiField_apply
+theorem nnnorm_smulRight (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
+    ‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊ := by
+  refine le_antisymm ?_ ?_
+  · refine (opNNNorm_le_iff _ |>.2 fun m => (nnnorm_smul_le _ _).trans ?_)
+    rw [mul_right_comm]
+    gcongr
+    exact le_opNNNorm _ _
+  · obtain hz | hz := eq_or_ne ‖z‖₊ 0
+    · simp [hz]
+    rw [← NNReal.le_div_iff hz, opNNNorm_le_iff]
+    intro m
+    rw [div_mul_eq_mul_div, NNReal.le_div_iff hz]
+    refine le_trans ?_ ((f.smulRight z).le_opNNNorm m)
+    rw [smulRight_apply, nnnorm_smul]
 
-theorem mkPiField_apply_one_eq_self (f : ContinuousMultilinearMap 𝕜 (fun _ : ι => 𝕜) G) :
-    ContinuousMultilinearMap.mkPiField 𝕜 ι (f fun _ => 1) = f :=
-  toMultilinearMap_injective f.toMultilinearMap.mkPiRing_apply_one_eq_self
-#align continuous_multilinear_map.mk_pi_field_apply_one_eq_self ContinuousMultilinearMap.mkPiField_apply_one_eq_self
+@[simp]
+theorem norm_smulRight (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
+    ‖f.smulRight z‖ = ‖f‖ * ‖z‖ :=
+  congr_arg NNReal.toReal (nnnorm_smulRight f z)
 
 @[simp]
-theorem norm_mkPiField (z : G) : ‖ContinuousMultilinearMap.mkPiField 𝕜 ι z‖ = ‖z‖ :=
-  (MultilinearMap.mkContinuous_norm_le _ (norm_nonneg z) _).antisymm <| by
-    simpa using (ContinuousMultilinearMap.mkPiField 𝕜 ι z).le_opNorm fun _ => 1
-#align continuous_multilinear_map.norm_mk_pi_field ContinuousMultilinearMap.norm_mkPiField
-
-theorem mkPiField_eq_iff {z₁ z₂ : G} :
-    ContinuousMultilinearMap.mkPiField 𝕜 ι z₁ = ContinuousMultilinearMap.mkPiField 𝕜 ι z₂ ↔
-      z₁ = z₂ := by
-  rw [← toMultilinearMap_injective.eq_iff]
-  exact MultilinearMap.mkPiRing_eq_iff
-#align continuous_multilinear_map.mk_pi_field_eq_iff ContinuousMultilinearMap.mkPiField_eq_iff
-
-theorem mkPiField_zero : ContinuousMultilinearMap.mkPiField 𝕜 ι (0 : G) = 0 := by
-  ext; rw [mkPiField_apply, smul_zero, ContinuousMultilinearMap.zero_apply]
-#align continuous_multilinear_map.mk_pi_field_zero ContinuousMultilinearMap.mkPiField_zero
-
-theorem mkPiField_eq_zero_iff (z : G) : ContinuousMultilinearMap.mkPiField 𝕜 ι z = 0 ↔ z = 0 := by
-  rw [← mkPiField_zero, mkPiField_eq_iff]
-#align continuous_multilinear_map.mk_pi_field_eq_zero_iff ContinuousMultilinearMap.mkPiField_eq_zero_iff
+theorem norm_mkPiRing (z : G) : ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖ := by
+  rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]
+#align continuous_multilinear_map.norm_mk_pi_field ContinuousMultilinearMap.norm_mkPiRing
 
 variable (𝕜 ι G)
 
@@ -966,7 +949,7 @@ continuous multilinear map is completely determined by its value on the constant
 ones. We register this bijection as a linear isometry in
 `ContinuousMultilinearMap.piFieldEquiv`. -/
 protected def piFieldEquiv : G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun _ : ι => 𝕜) G where
-  toFun z := ContinuousMultilinearMap.mkPiField 𝕜 ι z
+  toFun z := ContinuousMultilinearMap.mkPiRing 𝕜 ι z
   invFun f := f fun i => 1
   map_add' z z' := by
     ext m
@@ -975,8 +958,8 @@ protected def piFieldEquiv : G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fu
     ext m
     simp [smul_smul, mul_comm]
   left_inv z := by simp
-  right_inv f := f.mkPiField_apply_one_eq_self
-  norm_map' := norm_mkPiField
+  right_inv f := f.mkPiRing_apply_one_eq_self
+  norm_map' := norm_mkPiRing
 #align continuous_multilinear_map.pi_field_equiv ContinuousMultilinearMap.piFieldEquiv
 
 end ContinuousMultilinearMap

Mathlib/Analysis/NormedSpace/Spectrum.lean

@@ -263,11 +263,11 @@ power series with coefficients `a ^ n` represents the function `(1 - z • a)⁻
 radius `‖a‖₊⁻¹`. -/
 theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [CompleteSpace A] (a : A) :
     HasFPowerSeriesOnBall (fun z : 𝕜 => Ring.inverse (1 - z • a))
-      (fun n => ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (a ^ n)) 0 ‖a‖₊⁻¹ :=
+      (fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 ‖a‖₊⁻¹ :=
   { r_le := by
       refine'
         le_of_forall_nnreal_lt fun r hr => le_radius_of_bound_nnreal _ (max 1 ‖(1 : A)‖₊) fun n => _
-      rw [← norm_toNNReal, norm_mkPiField, norm_toNNReal]
+      rw [← norm_toNNReal, norm_mkPiRing, norm_toNNReal]
       cases' n with n
       · simp only [Nat.zero_eq, le_refl, mul_one, or_true_iff, le_max_iff, pow_zero]
       · refine'
@@ -336,10 +336,10 @@ theorem limsup_pow_nnnorm_pow_one_div_le_spectralRadius (a : A) :
   refine' ENNReal.inv_le_inv.mp (le_of_forall_pos_nnreal_lt fun r r_pos r_lt => _)
   simp_rw [inv_limsup, ← one_div]
   let p : FormalMultilinearSeries ℂ ℂ A := fun n =>
-    ContinuousMultilinearMap.mkPiField ℂ (Fin n) (a ^ n)
+    ContinuousMultilinearMap.mkPiRing ℂ (Fin n) (a ^ n)
   suffices h : (r : ℝ≥0∞) ≤ p.radius
   · convert h
-    simp only [p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiField]
+    simp only [p.radius_eq_liminf, ← norm_toNNReal, norm_mkPiRing]
     congr
     ext n
     rw [norm_toNNReal, ENNReal.coe_rpow_def ‖a ^ n‖₊ (1 / n : ℝ), if_neg]

Mathlib/MeasureTheory/Integral/CircleIntegral.lean

@@ -522,14 +522,14 @@ series converges to `f w` if `f` is differentiable on the closed ball `Metric.cl
 `w` belongs to the corresponding open ball. For any circle integrable function `f`, this power
 series converges to the Cauchy integral for `f`. -/
 def cauchyPowerSeries (f : ℂ → E) (c : ℂ) (R : ℝ) : FormalMultilinearSeries ℂ ℂ E := fun n =>
-  ContinuousMultilinearMap.mkPiField ℂ _ <|
+  ContinuousMultilinearMap.mkPiRing ℂ _ <|
     (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z
 #align cauchy_power_series cauchyPowerSeries
 
 theorem cauchyPowerSeries_apply (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) (w : ℂ) :
     (cauchyPowerSeries f c R n fun _ => w) =
       (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z := by
-  simp only [cauchyPowerSeries, ContinuousMultilinearMap.mkPiField_apply, Fin.prod_const,
+  simp only [cauchyPowerSeries, ContinuousMultilinearMap.mkPiRing_apply, Fin.prod_const,
     div_eq_mul_inv, mul_pow, mul_smul, circleIntegral.integral_smul]
   rw [← smul_comm (w ^ n)]
 #align cauchy_power_series_apply cauchyPowerSeries_apply

Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

@@ -650,4 +650,46 @@ def smulRight : ContinuousMultilinearMap R M₁ M₂ where
 
 end SMulRight
 
+section CommRing
+variable {M : Type*}
+variable [Fintype ι] [CommRing R] [AddCommMonoid M] [Module R M]
+variable [TopologicalSpace R] [TopologicalSpace M]
+variable [ContinuousMul R] [ContinuousSMul R M]
+
+variable (R ι) in
+/-- The canonical continuous multilinear map on `R^ι`, associating to `m` the product of all the
+`m i` (multiplied by a fixed reference element `z` in the target module) -/
+protected def mkPiRing (z : M) : ContinuousMultilinearMap R (fun _ : ι => R) M :=
+  (ContinuousMultilinearMap.mkPiAlgebra R ι R).smulRight z
+#align continuous_multilinear_map.mk_pi_field ContinuousMultilinearMap.mkPiRing
+
+
+@[simp]
+theorem mkPiRing_apply (z : M) (m : ι → R) :
+    (ContinuousMultilinearMap.mkPiRing R ι z : (ι → R) → M) m = (∏ i, m i) • z :=
+  rfl
+#align continuous_multilinear_map.mk_pi_field_apply ContinuousMultilinearMap.mkPiRing_apply
+
+theorem mkPiRing_apply_one_eq_self (f : ContinuousMultilinearMap R (fun _ : ι => R) M) :
+    ContinuousMultilinearMap.mkPiRing R ι (f fun _ => 1) = f :=
+  toMultilinearMap_injective f.toMultilinearMap.mkPiRing_apply_one_eq_self
+#align continuous_multilinear_map.mk_pi_field_apply_one_eq_self ContinuousMultilinearMap.mkPiRing_apply_one_eq_self
+
+theorem mkPiRing_eq_iff {z₁ z₂ : M} :
+    ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔
+      z₁ = z₂ := by
+  rw [← toMultilinearMap_injective.eq_iff]
+  exact MultilinearMap.mkPiRing_eq_iff
+#align continuous_multilinear_map.mk_pi_field_eq_iff ContinuousMultilinearMap.mkPiRing_eq_iff
+
+theorem mkPiRing_zero : ContinuousMultilinearMap.mkPiRing R ι (0 : M) = 0 := by
+  ext; rw [mkPiRing_apply, smul_zero, ContinuousMultilinearMap.zero_apply]
+#align continuous_multilinear_map.mk_pi_field_zero ContinuousMultilinearMap.mkPiRing_zero
+
+theorem mkPiRing_eq_zero_iff (z : M) : ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0 := by
+  rw [← mkPiRing_zero, mkPiRing_eq_iff]
+#align continuous_multilinear_map.mk_pi_field_eq_zero_iff ContinuousMultilinearMap.mkPiRing_eq_zero_iff
+
+end CommRing
+
 end ContinuousMultilinearMap