feat(Analysis/Normed): Class for strict multiplicativity of norm

Mathlib/Analysis/Asymptotics/Defs.lean

@@ -58,6 +58,7 @@ variable [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddC
   [SeminormedAddGroup E''']
   [SeminormedRing R']
 
+variable {S : Type*} [NormedRing S] [NormMulClass S]
 variable [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜']
 variable {c c' c₁ c₂ : ℝ} {f : α → E} {g : α → F} {k : α → G}
 variable {f' : α → E'} {g' : α → F'} {k' : α → G'}
@@ -1127,26 +1128,26 @@ theorem isBigOWith_self_const_mul' (u : Rˣ) (f : α → R) (l : Filter α) :
   (isBigOWith_const_mul_self ↑u⁻¹ (fun x ↦ ↑u * f x) l).congr_left
     fun x ↦ u.inv_mul_cancel_left (f x)
 
-theorem isBigOWith_self_const_mul (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : Filter α) :
-    IsBigOWith ‖c‖⁻¹ l f fun x => c * f x :=
-  (isBigOWith_self_const_mul' (Units.mk0 c hc) f l).congr_const <| norm_inv c
+theorem isBigOWith_self_const_mul {c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) :
+    IsBigOWith ‖c‖⁻¹ l f fun x ↦ c * f x := by
+  simp [IsBigOWith, inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr hc)]
 
 theorem isBigO_self_const_mul' {c : R} (hc : IsUnit c) (f : α → R) (l : Filter α) :
     f =O[l] fun x => c * f x :=
   let ⟨u, hu⟩ := hc
   hu ▸ (isBigOWith_self_const_mul' u f l).isBigO
 
-theorem isBigO_self_const_mul (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : Filter α) :
-    f =O[l] fun x => c * f x :=
-  isBigO_self_const_mul' (IsUnit.mk0 c hc) f l
+theorem isBigO_self_const_mul {c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) :
+    f =O[l] fun x ↦ c * f x :=
+  (isBigOWith_self_const_mul hc f l).isBigO
 
 theorem isBigO_const_mul_left_iff' {f : α → R} {c : R} (hc : IsUnit c) :
     (fun x => c * f x) =O[l] g ↔ f =O[l] g :=
   ⟨(isBigO_self_const_mul' hc f l).trans, fun h => h.const_mul_left c⟩
 
-theorem isBigO_const_mul_left_iff {f : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
+theorem isBigO_const_mul_left_iff {f : α → S} {c : S} (hc : c ≠ 0) :
     (fun x => c * f x) =O[l] g ↔ f =O[l] g :=
-  isBigO_const_mul_left_iff' <| IsUnit.mk0 c hc
+  ⟨(isBigO_self_const_mul hc f l).trans, (isBigO_const_mul_self c f l).trans⟩
 
 theorem IsLittleO.const_mul_left {f : α → R} (h : f =o[l] g) (c : R) : (fun x => c * f x) =o[l] g :=
   (isBigO_const_mul_self c f l).trans_isLittleO h
@@ -1155,9 +1156,9 @@ theorem isLittleO_const_mul_left_iff' {f : α → R} {c : R} (hc : IsUnit c) :
     (fun x => c * f x) =o[l] g ↔ f =o[l] g :=
   ⟨(isBigO_self_const_mul' hc f l).trans_isLittleO, fun h => h.const_mul_left c⟩
 
-theorem isLittleO_const_mul_left_iff {f : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
+theorem isLittleO_const_mul_left_iff {f : α → S} {c : S} (hc : c ≠ 0) :
     (fun x => c * f x) =o[l] g ↔ f =o[l] g :=
-  isLittleO_const_mul_left_iff' <| IsUnit.mk0 c hc
+  ⟨(isBigO_self_const_mul hc f l).trans_isLittleO, (isBigO_const_mul_self c f l).trans_isLittleO⟩
 
 theorem IsBigOWith.of_const_mul_right {g : α → R} {c : R} (hc' : 0 ≤ c')
     (h : IsBigOWith c' l f fun x => c * g x) : IsBigOWith (c' * ‖c‖) l f g :=
@@ -1171,25 +1172,26 @@ theorem IsBigOWith.const_mul_right' {g : α → R} {u : Rˣ} {c' : ℝ} (hc' : 0
     (h : IsBigOWith c' l f g) : IsBigOWith (c' * ‖(↑u⁻¹ : R)‖) l f fun x => ↑u * g x :=
   h.trans (isBigOWith_self_const_mul' _ _ _) hc'
 
-theorem IsBigOWith.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) {c' : ℝ} (hc' : 0 ≤ c')
+theorem IsBigOWith.const_mul_right {g : α → S} {c : S} (hc : c ≠ 0) {c' : ℝ} (hc' : 0 ≤ c')
     (h : IsBigOWith c' l f g) : IsBigOWith (c' * ‖c‖⁻¹) l f fun x => c * g x :=
-  h.trans (isBigOWith_self_const_mul c hc g l) hc'
+  h.trans (isBigOWith_self_const_mul hc g l) hc'
 
 theorem IsBigO.const_mul_right' {g : α → R} {c : R} (hc : IsUnit c) (h : f =O[l] g) :
     f =O[l] fun x => c * g x :=
   h.trans (isBigO_self_const_mul' hc g l)
 
-theorem IsBigO.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) (h : f =O[l] g) :
+theorem IsBigO.const_mul_right {g : α → S} {c : S} (hc : c ≠ 0) (h : f =O[l] g) :
     f =O[l] fun x => c * g x :=
-  h.const_mul_right' <| IsUnit.mk0 c hc
+  match h.exists_nonneg with
+  | ⟨_, hd, hd'⟩ => (hd'.const_mul_right hc hd).isBigO
 
 theorem isBigO_const_mul_right_iff' {g : α → R} {c : R} (hc : IsUnit c) :
     (f =O[l] fun x => c * g x) ↔ f =O[l] g :=
   ⟨fun h => h.of_const_mul_right, fun h => h.const_mul_right' hc⟩
 
-theorem isBigO_const_mul_right_iff {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
+theorem isBigO_const_mul_right_iff {g : α → S} {c : S} (hc : c ≠ 0) :
     (f =O[l] fun x => c * g x) ↔ f =O[l] g :=
-  isBigO_const_mul_right_iff' <| IsUnit.mk0 c hc
+  ⟨fun h ↦ h.of_const_mul_right, fun h ↦ h.const_mul_right hc⟩
 
 theorem IsLittleO.of_const_mul_right {g : α → R} {c : R} (h : f =o[l] fun x => c * g x) :
     f =o[l] g :=
@@ -1199,21 +1201,21 @@ theorem IsLittleO.const_mul_right' {g : α → R} {c : R} (hc : IsUnit c) (h : f
     f =o[l] fun x => c * g x :=
   h.trans_isBigO (isBigO_self_const_mul' hc g l)
 
-theorem IsLittleO.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) (h : f =o[l] g) :
+theorem IsLittleO.const_mul_right {g : α → S} {c : S} (hc : c ≠ 0) (h : f =o[l] g) :
     f =o[l] fun x => c * g x :=
-  h.const_mul_right' <| IsUnit.mk0 c hc
+  h.trans_isBigO <| isBigO_self_const_mul hc g l
 
 theorem isLittleO_const_mul_right_iff' {g : α → R} {c : R} (hc : IsUnit c) :
     (f =o[l] fun x => c * g x) ↔ f =o[l] g :=
   ⟨fun h => h.of_const_mul_right, fun h => h.const_mul_right' hc⟩
 
-theorem isLittleO_const_mul_right_iff {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
+theorem isLittleO_const_mul_right_iff {g : α → S} {c : S} (hc : c ≠ 0) :
     (f =o[l] fun x => c * g x) ↔ f =o[l] g :=
-  isLittleO_const_mul_right_iff' <| IsUnit.mk0 c hc
+  ⟨fun h ↦ h.of_const_mul_right, fun h ↦ h.trans_isBigO (isBigO_self_const_mul hc g l)⟩
 
 /-! ### Multiplication -/
 
-theorem IsBigOWith.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} {c₁ c₂ : ℝ} (h₁ : IsBigOWith c₁ l f₁ g₁)
+theorem IsBigOWith.mul {f₁ f₂ : α → R} {g₁ g₂ : α → S} {c₁ c₂ : ℝ} (h₁ : IsBigOWith c₁ l f₁ g₁)
     (h₂ : IsBigOWith c₂ l f₂ g₂) :
     IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x := by
   simp only [IsBigOWith_def] at *
@@ -1222,44 +1224,46 @@ theorem IsBigOWith.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} {c₁ c
   convert mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
   rw [norm_mul, mul_mul_mul_comm]
 
-theorem IsBigO.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂) :
+theorem IsBigO.mul {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂) :
     (fun x => f₁ x * f₂ x) =O[l] fun x => g₁ x * g₂ x :=
   let ⟨_c, hc⟩ := h₁.isBigOWith
   let ⟨_c', hc'⟩ := h₂.isBigOWith
   (hc.mul hc').isBigO
 
-theorem IsBigO.mul_isLittleO {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =o[l] g₂) :
+theorem IsBigO.mul_isLittleO {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =o[l] g₂) :
     (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x := by
   simp only [IsLittleO_def] at *
   intro c cpos
   rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩
   exact (hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))
 
-theorem IsLittleO.mul_isBigO {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =O[l] g₂) :
-    (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x := by
+theorem IsLittleO.mul_isBigO {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =O[l] g₂) :
+    (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x := by
   simp only [IsLittleO_def] at *
   intro c cpos
   rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩
   exact ((h₁ (div_pos cpos c'pos)).mul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))
 
-theorem IsLittleO.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
-    (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x :=
+theorem IsLittleO.mul {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
+    (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x :=
   h₁.mul_isBigO h₂.isBigO
 
-theorem IsBigOWith.pow' {f : α → R} {g : α → 𝕜} (h : IsBigOWith c l f g) :
-    ∀ n : ℕ, IsBigOWith (Nat.casesOn n ‖(1 : R)‖ fun n => c ^ (n + 1))
+theorem IsBigOWith.pow' [Nontrivial S] {f : α → R} {g : α → S} (h : IsBigOWith c l f g) :
+    ∀ n : ℕ, IsBigOWith (Nat.casesOn n ‖(1 : R)‖ fun n ↦ c ^ (n + 1))
       l (fun x => f x ^ n) fun x => g x ^ n
-  | 0 => by simpa using isBigOWith_const_const (1 : R) (one_ne_zero' 𝕜) l
+  | 0 => by simpa using isBigOWith_const_const (1 : R) (one_ne_zero' S) l
   | 1 => by simpa
   | n + 2 => by simpa [pow_succ] using (IsBigOWith.pow' h (n + 1)).mul h
 
-theorem IsBigOWith.pow [NormOneClass R] {f : α → R} {g : α → 𝕜} (h : IsBigOWith c l f g) :
+theorem IsBigOWith.pow [Nontrivial S] [NormOneClass R]
+    {f : α → R} {g : α → S} (h : IsBigOWith c l f g) :
     ∀ n : ℕ, IsBigOWith (c ^ n) l (fun x => f x ^ n) fun x => g x ^ n
   | 0 => by simpa using h.pow' 0
   | n + 1 => h.pow' (n + 1)
 
-theorem IsBigOWith.of_pow {n : ℕ} {f : α → 𝕜} {g : α → R} (h : IsBigOWith c l (f ^ n) (g ^ n))
-    (hn : n ≠ 0) (hc : c ≤ c' ^ n) (hc' : 0 ≤ c') : IsBigOWith c' l f g :=
+theorem IsBigOWith.of_pow [Nontrivial S] {n : ℕ} {f : α → S} {g : α → R}
+    (h : IsBigOWith c l (f ^ n) (g ^ n)) (hn : n ≠ 0) (hc : c ≤ c' ^ n) (hc' : 0 ≤ c') :
+    IsBigOWith c' l f g :=
   IsBigOWith.of_bound <| (h.weaken hc).bound.mono fun x hx ↦
     le_of_pow_le_pow_left₀ hn (by positivity) <|
       calc
@@ -1268,20 +1272,20 @@ theorem IsBigOWith.of_pow {n : ℕ} {f : α → 𝕜} {g : α → R} (h : IsBigO
         _ ≤ c' ^ n * ‖g x‖ ^ n := by gcongr; exact norm_pow_le' _ hn.bot_lt
         _ = (c' * ‖g x‖) ^ n := (mul_pow _ _ _).symm
 
-theorem IsBigO.pow {f : α → R} {g : α → 𝕜} (h : f =O[l] g) (n : ℕ) :
+theorem IsBigO.pow [Nontrivial S] {f : α → R} {g : α → S} (h : f =O[l] g) (n : ℕ) :
     (fun x => f x ^ n) =O[l] fun x => g x ^ n :=
   let ⟨_C, hC⟩ := h.isBigOWith
   isBigO_iff_isBigOWith.2 ⟨_, hC.pow' n⟩
 
-theorem IsLittleO.pow {f : α → R} {g : α → 𝕜} (h : f =o[l] g) {n : ℕ} (hn : 0 < n) :
+theorem IsLittleO.pow {f : α → R} {g : α → S} (h : f =o[l] g) {n : ℕ} (hn : 0 < n) :
     (fun x => f x ^ n) =o[l] fun x => g x ^ n := by
   obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'; clear hn
   induction n with
   | zero => simpa only [pow_one]
   | succ n ihn => convert ihn.mul h <;> simp [pow_succ]
 
-theorem IsLittleO.of_pow {f : α → 𝕜} {g : α → R} {n : ℕ} (h : (f ^ n) =o[l] (g ^ n)) (hn : n ≠ 0) :
-    f =o[l] g :=
+theorem IsLittleO.of_pow [Nontrivial S] {f : α → S} {g : α → R} {n : ℕ}
+    (h : (f ^ n) =o[l] (g ^ n)) (hn : n ≠ 0) : f =o[l] g :=
   IsLittleO.of_isBigOWith fun _c hc => (h.def' <| pow_pos hc _).of_pow hn le_rfl hc.le
 
 /-! ### Inverse -/

Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

@@ -596,8 +596,9 @@ instance instNormedSpace : NormedSpace ℂ (CStarMatrix m n A) :=
 
 noncomputable instance instNonUnitalNormedRing :
     NonUnitalNormedRing (CStarMatrix n n A) where
-  dist_eq _ _ := rfl
-  norm_mul _ _ := by simpa only [norm_def', map_mul] using norm_mul_le _ _
+  __ : NormedAddCommGroup (CStarMatrix n n A) := inferInstance
+  __ : NonUnitalRing (CStarMatrix n n A) := inferInstance
+  norm_mul_le _ _ := by simpa only [norm_def', map_mul] using norm_mul_le _ _
 
 open ContinuousLinearMap CStarModule in
 /-- Matrices with entries in a C⋆-algebra form a C⋆-algebra. -/
@@ -649,7 +650,7 @@ variable {n : Type*} [Fintype n] [DecidableEq n]
 
 noncomputable instance instNormedRing : NormedRing (CStarMatrix n n A) where
   dist_eq _ _ := rfl
-  norm_mul := norm_mul_le
+  norm_mul_le := norm_mul_le
 
 noncomputable instance instNormedAlgebra : NormedAlgebra ℂ (CStarMatrix n n A) where
   norm_smul_le r M := by simpa only [norm_def, map_smul] using (toCLM M).opNorm_smul_le r

Mathlib/Analysis/CStarAlgebra/Matrix.lean

@@ -225,7 +225,7 @@ scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedSpace
 identification with (continuous) linear endmorphisms of `EuclideanSpace 𝕜 n`. -/
 def instL2OpNormedRing : NormedRing (Matrix n n 𝕜) where
   dist_eq := l2OpNormedRingAux.dist_eq
-  norm_mul := l2OpNormedRingAux.norm_mul
+  norm_mul_le := l2OpNormedRingAux.norm_mul_le
 
 scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedRing
 

Mathlib/Analysis/CStarAlgebra/Multiplier.lean

@@ -506,12 +506,8 @@ theorem norm_def' (a : 𝓜(𝕜, A)) : ‖a‖ = ‖toProdMulOppositeHom a‖ :
 theorem nnnorm_def' (a : 𝓜(𝕜, A)) : ‖a‖₊ = ‖toProdMulOppositeHom a‖₊ :=
   rfl
 
-instance instNormedSpace : NormedSpace 𝕜 𝓜(𝕜, A) :=
-  { DoubleCentralizer.instModule with
-    norm_smul_le := fun k a => (norm_smul_le k a.toProdMulOpposite :) }
-
-instance instNormedAlgebra : NormedAlgebra 𝕜 𝓜(𝕜, A) :=
-  { DoubleCentralizer.instAlgebra, DoubleCentralizer.instNormedSpace with }
+instance instNormedAlgebra : NormedAlgebra 𝕜 𝓜(𝕜, A) where
+  norm_smul_le k a := norm_smul_le k a.toProdMulOpposite
 
 theorem isUniformEmbedding_toProdMulOpposite :
     IsUniformEmbedding (toProdMulOpposite (𝕜 := 𝕜) (A := A)) :=

Mathlib/Analysis/CStarAlgebra/lpSpace.lean

@@ -27,7 +27,7 @@ instance [∀ i, NonUnitalCommCStarAlgebra (A i)] : NonUnitalCommCStarAlgebra (l
 -- aside from `∀ i, NormOneClass (A i)`, this holds automatically for C⋆-algebras though.
 instance [∀ i, Nontrivial (A i)] [∀ i, CStarAlgebra (A i)] : NormedRing (lp A ∞) where
   dist_eq := dist_eq_norm
-  norm_mul := norm_mul_le
+  norm_mul_le := norm_mul_le
 
 instance [∀ i, Nontrivial (A i)] [∀ i, CommCStarAlgebra (A i)] : CommCStarAlgebra (lp A ∞) where
   mul_comm := mul_comm

Mathlib/Analysis/Complex/Basic.lean

@@ -50,7 +50,7 @@ open ComplexConjugate Topology Filter
 
 instance : NormedField ℂ where
   dist_eq _ _ := rfl
-  norm_mul' := Complex.norm_mul
+  norm_mul := Complex.norm_mul
 
 instance : DenselyNormedField ℂ where
   lt_norm_lt r₁ r₂ h₀ hr :=

Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

@@ -136,7 +136,7 @@ theorem balancedHull.balanced (s : Set E) : Balanced 𝕜 (balancedHull 𝕜 s)
   simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]
   rintro x ⟨r, hr, hx⟩
   rw [← smul_assoc] at hx
-  exact ⟨a • r, (SeminormedRing.norm_mul _ _).trans (mul_le_one₀ ha (norm_nonneg r) hr), hx⟩
+  exact ⟨a • r, (norm_mul_le _ _).trans (mul_le_one₀ ha (norm_nonneg r) hr), hx⟩
 
 open Balanced in
 theorem balancedHull_add_subset [NormOneClass 𝕜] {t : Set E} :

Mathlib/Analysis/Matrix.lean

@@ -325,7 +325,7 @@ the norm of a matrix. -/
 protected def linftyOpNonUnitalSemiNormedRing [NonUnitalSeminormedRing α] :
     NonUnitalSeminormedRing (Matrix n n α) :=
   { Matrix.linftyOpSeminormedAddCommGroup, Matrix.instNonUnitalRing with
-    norm_mul := linfty_opNorm_mul }
+    norm_mul_le := linfty_opNorm_mul }
 
 /-- The `L₁-L∞` norm preserves one on non-empty matrices. Note this is safe as an instance, as it
 carries no data. -/
@@ -597,7 +597,7 @@ matrix. -/
 def frobeniusNormedRing [DecidableEq m] : NormedRing (Matrix m m α) :=
   { Matrix.frobeniusSeminormedAddCommGroup, Matrix.instRing with
     norm := Norm.norm
-    norm_mul := frobenius_norm_mul
+    norm_mul_le := frobenius_norm_mul
     eq_of_dist_eq_zero := eq_of_dist_eq_zero }
 
 /-- Normed algebra instance (using frobenius norm) for matrices over `ℝ` or `ℂ`.  Not

Mathlib/Analysis/Normed/Algebra/Spectrum.lean

@@ -446,7 +446,7 @@ theorem algebraMap_eq_of_mem {a : A} {z : ℂ} (h : z ∈ σ a) : algebraMap ℂ
 is an algebra isomorphism whose inverse is given by selecting the (unique) element of
 `spectrum ℂ a`. In addition, `algebraMap_isometry` guarantees this map is an isometry.
 
-Note: because `NormedDivisionRing` requires the field `norm_mul' : ∀ a b, ‖a * b‖ = ‖a‖ * ‖b‖`, we
+Note: because `NormedDivisionRing` requires the field `norm_mul : ∀ a b, ‖a * b‖ = ‖a‖ * ‖b‖`, we
 don't use this type class and instead opt for a `NormedRing` in which the nonzero elements are
 precisely the units. This allows for the application of this isomorphism in broader contexts, e.g.,
 to the quotient of a complex Banach algebra by a maximal ideal. In the case when `A` is actually a

Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean

@@ -220,20 +220,19 @@ variable [Module R M] [IsBoundedSMul R M] [Module Rᵐᵒᵖ M] [IsBoundedSMul R
   [SMulCommClass R Rᵐᵒᵖ M]
 
 instance instL1SeminormedRing : SeminormedRing (tsze R M) where
-  norm_mul
+  norm_mul_le
   | ⟨r₁, m₁⟩, ⟨r₂, m₂⟩ => by
-    dsimp
-    rw [norm_def, norm_def, norm_def, add_mul, mul_add, mul_add, snd_mul, fst_mul]
-    dsimp [fst, snd]
-    rw [add_assoc]
-    gcongr
-    · exact norm_mul_le _ _
-    refine (norm_add_le _ _).trans ?_
-    gcongr
-    · exact norm_smul_le _ _
-    refine (_root_.norm_smul_le _ _).trans ?_
-    rw [mul_comm, MulOpposite.norm_op]
-    exact le_add_of_nonneg_right <| by positivity
+    simp_rw [norm_def]
+    calc ‖r₁ * r₂‖ + ‖r₁ • m₂ + MulOpposite.op r₂ • m₁‖
+    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) := by
+      gcongr
+      · apply norm_mul_le
+      · refine norm_add_le_of_le ?_ ?_ <;>
+        apply norm_smul_le
+    _ ≤ ‖r₁‖ * ‖r₂‖ + (‖r₁‖ * ‖m₂‖ + ‖r₂‖ * ‖m₁‖) + (‖m₁‖ * ‖m₂‖) := by
+      apply le_add_of_nonneg_right
+      positivity
+    _ = (‖r₁‖ + ‖m₁‖) * (‖r₂‖ + ‖m₂‖) := by ring
   __ : SeminormedAddCommGroup (tsze R M) := inferInstance
   __ : Ring (tsze R M) := inferInstance
 

Mathlib/Analysis/Normed/Algebra/Unitization.lean

@@ -232,7 +232,7 @@ noncomputable instance instMetricSpace : MetricSpace (Unitization 𝕜 A) :=
 algebra homomorphism `Unitization.splitMul 𝕜 A`. -/
 noncomputable instance instNormedRing : NormedRing (Unitization 𝕜 A) where
   dist_eq := normedRingAux.dist_eq
-  norm_mul := normedRingAux.norm_mul
+  norm_mul_le := normedRingAux.norm_mul_le
   norm := normedRingAux.norm
 
 /-- Pull back the normed algebra structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the

Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

@@ -110,7 +110,7 @@ def unitizationAlgEquiv (R : Type*) [CommSemiring R] [Algebra R 𝕜] [DistribMu
 
 noncomputable instance instUnitizationNormedRing : NormedRing (WithLp 1 (Unitization 𝕜 A)) where
   dist_eq := dist_eq_norm
-  norm_mul x y := by
+  norm_mul_le x y := by
     simp_rw [unitization_norm_def, add_mul, mul_add, unitization_mul, fst_mul, snd_mul]
     rw [add_assoc, add_assoc]
     gcongr