feat: add @[simp] lemma Prod.norm_mk (#20411)

leanprover-community · Jan 6, 2025 · 2f1f7b9 · 2f1f7b9
1 parent ac937ee
commit 2f1f7b9
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 5 deletions.
diff --git a/Mathlib/Analysis/Normed/Group/Constructions.lean b/Mathlib/Analysis/Normed/Group/Constructions.lean
@@ -229,6 +229,8 @@ instance Prod.toNorm : Norm (E × F) where norm x := ‖x.1‖ ⊔ ‖x.2‖
 
 lemma Prod.norm_def (x : E × F) : ‖x‖ = max ‖x.1‖ ‖x.2‖ := rfl
 
+@[simp] lemma Prod.norm_mk (x : E) (y : F) : ‖(x, y)‖ = max ‖x‖ ‖y‖ := rfl
+
 lemma norm_fst_le (x : E × F) : ‖x.1‖ ≤ ‖x‖ := le_max_left _ _
 
 lemma norm_snd_le (x : E × F) : ‖x.2‖ ≤ ‖x‖ := le_max_right _ _
@@ -246,8 +248,16 @@ instance Prod.seminormedGroup : SeminormedGroup (E × F) where
   dist_eq x y := by
     simp only [Prod.norm_def, Prod.dist_eq, dist_eq_norm_div, Prod.fst_div, Prod.snd_div]
 
-@[to_additive Prod.nnnorm_def']
-lemma Prod.nnorm_def (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊ := rfl
+/-- Multiplicative version of `Prod.nnnorm_def`.
+Earlier, this names was used for the additive version. -/
+@[to_additive Prod.nnnorm_def]
+lemma Prod.nnnorm_def' (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊ := rfl
+
+@[deprecated (since := "2025-01-02")] alias Prod.nnorm_def := Prod.nnnorm_def'
+
+/-- Multiplicative version of `Prod.nnnorm_mk`. -/
+@[to_additive (attr := simp) Prod.nnnorm_mk]
+lemma Prod.nnnorm_mk' (x : E) (y : F) : ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊ := rfl
 
 end SeminormedGroup
 

diff --git a/Mathlib/Analysis/Normed/Lp/ProdLp.lean b/Mathlib/Analysis/Normed/Lp/ProdLp.lean
@@ -616,7 +616,7 @@ theorem prod_nnnorm_eq_sup (f : WithLp ∞ (α × β)) : ‖f‖₊ = ‖f.fst
   norm_cast
 
 @[simp] theorem prod_nnnorm_equiv (f : WithLp ∞ (α × β)) : ‖WithLp.equiv ⊤ _ f‖₊ = ‖f‖₊ := by
-  rw [prod_nnnorm_eq_sup, Prod.nnnorm_def', equiv_fst, equiv_snd]
+  rw [prod_nnnorm_eq_sup, Prod.nnnorm_def, equiv_fst, equiv_snd]
 
 @[simp] theorem prod_nnnorm_equiv_symm (f : α × β) : ‖(WithLp.equiv ⊤ _).symm f‖₊ = ‖f‖₊ :=
   (prod_nnnorm_equiv _).symm

diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
@@ -535,7 +535,7 @@ theorem isLeast_opNNNorm (f : ContinuousMultilinearMap 𝕜 E G) :
 theorem opNNNorm_prod (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
     ‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊ :=
   eq_of_forall_ge_iff fun _ ↦ by
-    simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def', max_le_iff, forall_and]
+    simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def, max_le_iff, forall_and]
 
 theorem opNorm_prod (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') :
     ‖f.prod g‖ = max ‖f‖ ‖g‖ :=

diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -388,7 +388,7 @@ theorem nnnorm_eq_sup_normAtPlace (x : mixedSpace K) :
       (univ.image (fun w : {w : InfinitePlace K // IsComplex w} ↦ w.1)) := by
     ext; simp [isReal_or_isComplex]
   rw [this, sup_union, univ.sup_image, univ.sup_image,
-    Prod.nnnorm_def', Pi.nnnorm_def, Pi.nnnorm_def]
+    Prod.nnnorm_def, Pi.nnnorm_def, Pi.nnnorm_def]
   congr
   · ext w
     simp [normAtPlace_apply_isReal w.prop]