bump to nightly-2023-09-26-06

mathlib commit leanprover-community/mathlib@ce64cd3
leanprover-community · Sep 26, 2023 · 61f91ae · 61f91ae
1 parent 04d498c
commit 61f91ae
Show file tree

Hide file tree

Showing 4 changed files with 116 additions and 105 deletions.
diff --git a/Mathbin/Analysis/NormedSpace/Multilinear.lean b/Mathbin/Analysis/NormedSpace/Multilinear.lean
@@ -554,9 +554,10 @@ theorem op_norm_prod (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMult
 #align continuous_multilinear_map.op_norm_prod ContinuousMultilinearMap.op_norm_prod
 -/
 
-#print ContinuousMultilinearMap.norm_pi /-
-theorem norm_pi {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [∀ i', NormedAddCommGroup (E' i')]
-    [∀ i', NormedSpace 𝕜 (E' i')] (f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) : ‖pi f‖ = ‖f‖ :=
+#print ContinuousMultilinearMap.op_norm_pi /-
+theorem op_norm_pi {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'}
+    [∀ i', NormedAddCommGroup (E' i')] [∀ i', NormedSpace 𝕜 (E' i')]
+    (f : ∀ i', ContinuousMultilinearMap 𝕜 E (E' i')) : ‖pi f‖ = ‖f‖ :=
   by
   apply le_antisymm
   · refine' op_norm_le_bound _ (norm_nonneg f) fun m => _
@@ -568,7 +569,7 @@ theorem norm_pi {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [∀ i', N
     refine' op_norm_le_bound _ (norm_nonneg _) fun m => _
     refine' le_trans _ ((pi f).le_op_norm m)
     convert norm_le_pi_norm (fun j => f j m) i
-#align continuous_multilinear_map.norm_pi ContinuousMultilinearMap.norm_pi
+#align continuous_multilinear_map.norm_pi ContinuousMultilinearMap.op_norm_pi
 -/
 
 section
@@ -666,7 +667,7 @@ def piₗᵢ {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'} [∀ i', Norm
     { piEquiv with
       map_add' := fun f g => rfl
       map_smul' := fun c f => rfl }
-  norm_map' := norm_pi
+  norm_map' := op_norm_pi
 #align continuous_multilinear_map.piₗᵢ ContinuousMultilinearMap.piₗᵢ
 -/