fix(analysis/normed_space/basic): allow the zero ring to be a normed …

…algebra (#13544)

This replaces `norm_algebra_map_eq : ∀ x : 𝕜, ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥` with `norm_smul_le : ∀ (r : 𝕜) (x : 𝕜'), ∥r • x∥ ≤ ∥r∥ * ∥x∥` in `normed_algebra`. With this change, `normed_algebra` means nothing more than "a normed module that is also an algebra", which seems to be the only notion actually used in mathlib anyway. In practice, this change really just removes any constraints on `∥1∥`.

The old meaning of `[normed_algebra R A]` is now achieved with `[normed_algebra R A] [norm_one_class A]`.
As a result, lemmas like `normed_algebra.norm_one_class` and `normed_algebra.nontrivial` have been removed, as they no longer make sense now that the two typeclasses are entirely orthogonal.

Notably this means that the following `normed_algebra` instances hold more generally than before:

* `continuous_linear_map.to_normed_algebra`
* `pi.normed_algebra`
* `bounded_continuous_function.normed_algebra`
* `continuous_map.normed_algebra`
* Instances not yet in mathlib:
  * Matrices under the `L1-L_inf` norm are a normed algebra even if the matrix is empty
  * Matrices under the frobenius norm are a normed algebra (note `∥(1 : matrix n n 𝕜')∥ = \sqrt (fintype.card n)` with that norm)

This last one is the original motivation for this PR; otherwise every lemma about a matrix exponential has to case on whether the matrices are empty.

It is possible that some of the `[norm_one_class A]`s added in `spectrum.lean` are unnecessary; however, the assumptions are no stronger than they were before, and I'm not interested in trying to generalize them as part of this PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Is.20the.20zero.20algebra.20normed.3F/near/279515954)

src/analysis/complex/basic.lean

@@ -37,6 +37,8 @@ open_locale complex_conjugate
 
 instance : has_norm ℂ := ⟨abs⟩
 
+@[simp] lemma norm_eq_abs (z : ℂ) : ∥z∥ = abs z := rfl
+
 instance : normed_group ℂ :=
 normed_group.of_core ℂ
 { norm_eq_zero_iff := λ z, abs_eq_zero,
@@ -50,10 +52,14 @@ instance : normed_field ℂ :=
   .. complex.field }
 
 instance : nondiscrete_normed_field ℂ :=
-{ non_trivial := ⟨2, by simp [norm]; norm_num⟩ }
+{ non_trivial := ⟨2, by simp; norm_num⟩ }
 
 instance {R : Type*} [normed_field R] [normed_algebra R ℝ] : normed_algebra R ℂ :=
-{ norm_algebra_map_eq := λ x, (abs_of_real $ algebra_map R ℝ x).trans (norm_algebra_map_eq ℝ x),
+{ norm_smul_le := λ r x, begin
+    rw [norm_eq_abs, norm_eq_abs, ←algebra_map_smul ℝ r x, algebra.smul_def, abs_mul,
+      ←norm_algebra_map' ℝ r, coe_algebra_map, abs_of_real],
+    refl,
+  end,
   to_algebra := complex.algebra }
 
 /-- The module structure from `module.complex_to_real` is a normed space. -/
@@ -62,8 +68,6 @@ instance _root_.normed_space.complex_to_real {E : Type*} [normed_group E] [norme
   normed_space ℝ E :=
 normed_space.restrict_scalars ℝ ℂ E
 
-@[simp] lemma norm_eq_abs (z : ℂ) : ∥z∥ = abs z := rfl
-
 lemma dist_eq (z w : ℂ) : dist z w = abs (z - w) := rfl
 
 lemma dist_self_conj (z : ℂ) : dist z (conj z) = 2 * |z.im| :=

src/analysis/normed/normed_field.lean

@@ -111,6 +111,10 @@ attribute [simp] norm_one
 @[simp] lemma nnnorm_one [semi_normed_group α] [has_one α] [norm_one_class α] : ∥(1 : α)∥₊ = 1 :=
 nnreal.eq norm_one
 
+lemma norm_one_class.nontrivial (α : Type*) [semi_normed_group α] [has_one α] [norm_one_class α] :
+  nontrivial α :=
+nontrivial_of_ne 0 1 $ ne_of_apply_ne norm $ by simp
+
 @[priority 100] -- see Note [lower instance priority]
 instance semi_normed_comm_ring.to_comm_ring [β : semi_normed_comm_ring α] : comm_ring α := { ..β }
 
@@ -331,7 +335,7 @@ variables [normed_ring α]
 lemma units.norm_pos [nontrivial α] (x : αˣ) : 0 < ∥(x:α)∥ :=
 norm_pos_iff.mpr (units.ne_zero x)
 
-lemma units.nnorm_pos [nontrivial α] (x : αˣ) : 0 < ∥(x:α)∥₊ :=
+lemma units.nnnorm_pos [nontrivial α] (x : αˣ) : 0 < ∥(x:α)∥₊ :=
 x.norm_pos
 
 /-- Normed ring structure on the product of two normed rings, using the sup norm. -/

src/analysis/normed_space/basic.lean

@@ -338,52 +338,16 @@ end normed_space_nondiscrete
 
 section normed_algebra
 
-/-- A normed algebra `𝕜'` over `𝕜` is an algebra endowed with a norm for which the
-embedding of `𝕜` in `𝕜'` is an isometry. -/
+/-- A normed algebra `𝕜'` over `𝕜` is normed module that is also an algebra. -/
 class normed_algebra (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜']
   extends algebra 𝕜 𝕜' :=
-(norm_algebra_map_eq : ∀x:𝕜, ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥)
+(norm_smul_le : ∀ (r : 𝕜) (x : 𝕜'), ∥r • x∥ ≤ ∥r∥ * ∥x∥)
 
-@[simp] lemma norm_algebra_map_eq {𝕜 : Type*} (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜']
-  [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥ :=
-normed_algebra.norm_algebra_map_eq _
-
-@[simp] lemma nnorm_algebra_map_eq {𝕜 : Type*} (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜']
-  [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥₊ = ∥x∥₊ :=
-subtype.ext $ normed_algebra.norm_algebra_map_eq _
-
-/-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
-lemma algebra_map_isometry (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜']
-  [normed_algebra 𝕜 𝕜'] : isometry (algebra_map 𝕜 𝕜') :=
-begin
-  refine isometry_emetric_iff_metric.2 (λx y, _),
-  rw [dist_eq_norm, dist_eq_norm, ← ring_hom.map_sub, norm_algebra_map_eq],
-end
-
-variables (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜]
-
-/-- The inclusion of the base field in a normed algebra as a continuous linear map. -/
-@[simps]
-def algebra_map_clm [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] : 𝕜 →L[𝕜] 𝕜' :=
-{ to_fun := algebra_map 𝕜 𝕜',
-  map_add' := (algebra_map 𝕜 𝕜').map_add,
-  map_smul' := λ r x, by rw [algebra.id.smul_eq_mul, map_mul, ring_hom.id_apply, algebra.smul_def],
-  cont := (algebra_map_isometry 𝕜 𝕜').continuous }
-
-lemma algebra_map_clm_coe [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
-  (algebra_map_clm 𝕜 𝕜' : 𝕜 → 𝕜') = (algebra_map 𝕜 𝕜' : 𝕜 → 𝕜') := rfl
-
-lemma algebra_map_clm_to_linear_map [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
-  (algebra_map_clm 𝕜 𝕜').to_linear_map = algebra.linear_map 𝕜 𝕜' := rfl
+variables {𝕜 : Type*} (𝕜' : Type*) [normed_field 𝕜] [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
 
 @[priority 100]
-instance normed_algebra.to_normed_space [semi_normed_ring 𝕜'] [h : normed_algebra 𝕜 𝕜'] :
-  normed_space 𝕜 𝕜' :=
-{ norm_smul_le := λ s x, calc
-    ∥s • x∥ = ∥((algebra_map 𝕜 𝕜') s) * x∥ : by { rw h.smul_def', refl }
-    ... ≤ ∥algebra_map 𝕜 𝕜' s∥ * ∥x∥ : semi_normed_ring.norm_mul _ _
-    ... = ∥s∥ * ∥x∥ : by rw norm_algebra_map_eq,
-  ..h }
+instance normed_algebra.to_normed_space : normed_space 𝕜 𝕜' :=
+{ norm_smul_le := normed_algebra.norm_smul_le }
 
 /-- While this may appear identical to `normed_algebra.to_normed_space`, it contains an implicit
 argument involving `normed_ring.to_semi_normed_ring` that typeclass inference has trouble inferring.
@@ -398,30 +362,55 @@ example
 
 See `normed_space.to_module'` for a similar situation. -/
 @[priority 100]
-instance normed_algebra.to_normed_space' [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
+instance normed_algebra.to_normed_space' {𝕜'} [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
   normed_space 𝕜 𝕜' := by apply_instance
 
-instance normed_algebra.id : normed_algebra 𝕜 𝕜 :=
-{ norm_algebra_map_eq := by simp,
-  .. algebra.id 𝕜}
+lemma norm_algebra_map (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥ * ∥(1 : 𝕜')∥ :=
+begin
+  rw algebra.algebra_map_eq_smul_one,
+  exact norm_smul _ _,
+end
 
-variables (𝕜') [semi_normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
-include 𝕜
+lemma nnnorm_algebra_map (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥₊ = ∥x∥₊ * ∥(1 : 𝕜')∥₊ :=
+subtype.ext $ norm_algebra_map 𝕜' x
 
-lemma normed_algebra.norm_one : ∥(1:𝕜')∥ = 1 :=
-by simpa using (norm_algebra_map_eq 𝕜' (1:𝕜))
+@[simp] lemma norm_algebra_map' [norm_one_class 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥ = ∥x∥ :=
+by rw [norm_algebra_map, norm_one, mul_one]
 
-lemma normed_algebra.norm_one_class : norm_one_class 𝕜' :=
-⟨normed_algebra.norm_one 𝕜 𝕜'⟩
+@[simp] lemma nnnorm_algebra_map' [norm_one_class 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜 𝕜' x∥₊ = ∥x∥₊ :=
+subtype.ext $ norm_algebra_map' _ _
 
-lemma normed_algebra.zero_ne_one : (0:𝕜') ≠ 1 :=
+variables (𝕜 𝕜')
+
+/-- In a normed algebra, the inclusion of the base field in the extended field is an isometry. -/
+lemma algebra_map_isometry [norm_one_class 𝕜'] : isometry (algebra_map 𝕜 𝕜') :=
 begin
-  refine (ne_zero_of_norm_ne_zero _).symm,
-  rw normed_algebra.norm_one 𝕜 𝕜', norm_num,
+  refine isometry_emetric_iff_metric.2 (λx y, _),
+  rw [dist_eq_norm, dist_eq_norm, ← ring_hom.map_sub, norm_algebra_map'],
 end
 
-lemma normed_algebra.nontrivial : nontrivial 𝕜' :=
-⟨⟨0, 1, normed_algebra.zero_ne_one 𝕜 𝕜'⟩⟩
+/-- The inclusion of the base field in a normed algebra as a continuous linear map. -/
+@[simps]
+def algebra_map_clm : 𝕜 →L[𝕜] 𝕜' :=
+{ to_fun := algebra_map 𝕜 𝕜',
+  map_add' := (algebra_map 𝕜 𝕜').map_add,
+  map_smul' := λ r x, by rw [algebra.id.smul_eq_mul, map_mul, ring_hom.id_apply, algebra.smul_def],
+  cont :=
+    have lipschitz_with ∥(1 : 𝕜')∥₊ (algebra_map 𝕜 𝕜') := λ x y, begin
+      rw [edist_eq_coe_nnnorm_sub, edist_eq_coe_nnnorm_sub, ←map_sub, ←ennreal.coe_mul,
+        ennreal.coe_le_coe, mul_comm],
+      exact (nnnorm_algebra_map _ _).le,
+    end, this.continuous }
+
+lemma algebra_map_clm_coe :
+  (algebra_map_clm 𝕜 𝕜' : 𝕜 → 𝕜') = (algebra_map 𝕜 𝕜' : 𝕜 → 𝕜') := rfl
+
+lemma algebra_map_clm_to_linear_map :
+  (algebra_map_clm 𝕜 𝕜').to_linear_map = algebra.linear_map 𝕜 𝕜' := rfl
+
+instance normed_algebra.id : normed_algebra 𝕜 𝕜 :=
+{ .. normed_field.to_normed_space,
+  .. algebra.id 𝕜}
 
 /-- Any normed characteristic-zero division ring that is a normed_algebra over the reals is also a
 normed algebra over the rationals.
@@ -430,27 +419,20 @@ Phrased another way, if `𝕜` is a normed algebra over the reals, then `algebra
 norm. -/
 instance normed_algebra_rat {𝕜} [normed_division_ring 𝕜] [char_zero 𝕜] [normed_algebra ℝ 𝕜] :
   normed_algebra ℚ 𝕜 :=
-{ norm_algebra_map_eq := λ q,
-    by simpa only [ring_hom.map_rat_algebra_map] using norm_algebra_map_eq 𝕜 (algebra_map _ ℝ q) }
+{ norm_smul_le := λ q x,
+    by rw [←smul_one_smul ℝ q x, rat.smul_one_eq_coe, norm_smul, rat.norm_cast_real], }
 
 /-- The product of two normed algebras is a normed algebra, with the sup norm. -/
 instance prod.normed_algebra {E F : Type*} [semi_normed_ring E] [semi_normed_ring F]
   [normed_algebra 𝕜 E] [normed_algebra 𝕜 F] :
   normed_algebra 𝕜 (E × F) :=
-{ norm_algebra_map_eq := λ x, begin
-    dsimp [prod.norm_def],
-    rw [norm_algebra_map_eq, norm_algebra_map_eq, max_self],
-  end }
+{ ..prod.normed_space }
 
 /-- The product of finitely many normed algebras is a normed algebra, with the sup norm. -/
-instance pi.normed_algebra {E : ι → Type*} [fintype ι] [nonempty ι]
+instance pi.normed_algebra {E : ι → Type*} [fintype ι]
   [Π i, semi_normed_ring (E i)] [Π i, normed_algebra 𝕜 (E i)] :
   normed_algebra 𝕜 (Π i, E i) :=
-{ norm_algebra_map_eq := λ x, begin
-    dsimp [has_norm.norm],
-    simp_rw [pi.algebra_map_apply ι E, nnorm_algebra_map_eq, ←coe_nnnorm],
-    rw finset.sup_const (@finset.univ_nonempty ι _ _) _,
-  end,
+{ .. pi.normed_space,
   .. pi.algebra _ E }
 
 end normed_algebra

src/analysis/normed_space/is_R_or_C.lean

@@ -30,7 +30,7 @@ open metric
 
 @[simp, is_R_or_C_simps] lemma is_R_or_C.norm_coe_norm {𝕜 : Type*} [is_R_or_C 𝕜]
   {E : Type*} [normed_group E] {z : E} : ∥(∥z∥ : 𝕜)∥ = ∥z∥ :=
-by { unfold_coes, simp only [norm_algebra_map_eq, ring_hom.to_fun_eq_coe, norm_norm], }
+by { unfold_coes, simp only [norm_algebra_map', ring_hom.to_fun_eq_coe, norm_norm], }
 
 variables {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [normed_group E] [normed_space 𝕜 E]
 

src/analysis/normed_space/operator_norm.lean

@@ -422,6 +422,12 @@ instance to_semi_normed_ring : semi_normed_ring (E →L[𝕜] E) :=
 { norm_mul := λ f g, op_norm_comp_le f g,
   .. continuous_linear_map.to_semi_normed_group }
 
+/-- For a normed space `E`, continuous linear endomorphisms form a normed algebra with
+respect to the operator norm. -/
+instance to_normed_algebra : normed_algebra 𝕜 (E →L[𝕜] E) :=
+{ .. continuous_linear_map.to_normed_space,
+  .. continuous_linear_map.algebra }
+
 theorem le_op_nnnorm : ∥f x∥₊ ≤ ∥f∥₊ * ∥x∥₊ := f.le_op_norm x
 
 /-- continuous linear maps are Lipschitz continuous. -/
@@ -774,45 +780,50 @@ variables {𝕜 E Fₗ Gₗ}
 section multiplication_linear
 variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
 
-/-- Left multiplication in a normed algebra as a linear isometry to the space of
-continuous linear maps. -/
-def lmulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-{ to_linear_map := (algebra.lmul 𝕜 𝕜').to_linear_map.mk_continuous₂ 1 $
-    λ x y, by simpa using norm_mul_le x y,
-  norm_map' := λ x, le_antisymm
-    (op_norm_le_bound _ (norm_nonneg x) (norm_mul_le x))
-    (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [normed_algebra.norm_one 𝕜 𝕜'],
-          apply_instance }) }
-
 /-- Left multiplication in a normed algebra as a continuous bilinear map. -/
 def lmul : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
-(lmulₗᵢ 𝕜 𝕜').to_continuous_linear_map
+(algebra.lmul 𝕜 𝕜').to_linear_map.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 coe_lmulₗᵢ : ⇑(lmulₗᵢ 𝕜 𝕜') = lmul 𝕜 𝕜' := rfl
+@[simp] lemma op_norm_lmul_apply_le (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ ≤ ∥x∥ :=
+(op_norm_le_bound _ (norm_nonneg x) (norm_mul_le x))
+
+/-- Left multiplication in a normed algebra as a linear isometry to the space of
+continuous linear maps. -/
+def lmulₗᵢ [norm_one_class 𝕜'] : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+{ to_linear_map := lmul 𝕜 𝕜',
+  norm_map' := λ x, le_antisymm (op_norm_lmul_apply_le _ _ _)
+    (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [norm_one],
+          apply_instance }) }
+
+@[simp] lemma coe_lmulₗᵢ [norm_one_class 𝕜'] : ⇑(lmulₗᵢ 𝕜 𝕜') = lmul 𝕜 𝕜' := rfl
 
-@[simp] lemma op_norm_lmul_apply (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ = ∥x∥ :=
+@[simp] lemma op_norm_lmul_apply [norm_one_class 𝕜'] (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ = ∥x∥ :=
 (lmulₗᵢ 𝕜 𝕜').norm_map x
 
 /-- Right-multiplication in a normed algebra, considered as a continuous linear map. -/
 def lmul_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' := (lmul 𝕜 𝕜').flip
 
 @[simp] lemma lmul_right_apply (x y : 𝕜') : lmul_right 𝕜 𝕜' x y = y * x := rfl
 
-@[simp] lemma op_norm_lmul_right_apply (x : 𝕜') : ∥lmul_right 𝕜 𝕜' x∥ = ∥x∥ :=
+@[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 _ _))
+
+@[simp] lemma op_norm_lmul_right_apply [norm_one_class 𝕜'] (x : 𝕜') : ∥lmul_right 𝕜 𝕜' x∥ = ∥x∥ :=
 le_antisymm
-  (op_norm_le_bound _ (norm_nonneg x) (λ y, (norm_mul_le y x).trans_eq (mul_comm _ _)))
-  (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [normed_algebra.norm_one 𝕜 𝕜'],
+  (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[𝕜] 𝕜' :=
+def lmul_rightₗᵢ [norm_one_class 𝕜'] : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
 { to_linear_map := lmul_right 𝕜 𝕜',
   norm_map' := op_norm_lmul_right_apply 𝕜 𝕜' }
 
-@[simp] lemma coe_lmul_rightₗᵢ : ⇑(lmul_rightₗᵢ 𝕜 𝕜') = lmul_right 𝕜 𝕜' := rfl
+@[simp] lemma coe_lmul_rightₗᵢ [norm_one_class 𝕜'] : ⇑(lmul_rightₗᵢ 𝕜 𝕜') = lmul_right 𝕜 𝕜' := rfl
 
 /-- Simultaneous left- and right-multiplication in a normed algebra, considered as a continuous
 trilinear map. -/
@@ -824,7 +835,9 @@ def lmul_left_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :
 
 lemma op_norm_lmul_left_right_apply_apply_le (x y : 𝕜') :
   ∥lmul_left_right 𝕜 𝕜' x y∥ ≤ ∥x∥ * ∥y∥ :=
-(op_norm_comp_le _ _).trans_eq $ by simp [mul_comm]
+(op_norm_comp_le _ _).trans $ (mul_comm _ _).trans_le $
+  mul_le_mul (op_norm_lmul_apply_le _ _ _) (op_norm_lmul_right_apply_le _ _ _)
+    (norm_nonneg _) (norm_nonneg _)
 
 lemma op_norm_lmul_left_right_apply_le (x : 𝕜') :
   ∥lmul_left_right 𝕜 𝕜' x∥ ≤ ∥x∥ :=
@@ -1252,13 +1265,6 @@ instance to_normed_ring : normed_ring (E →L[𝕜] E) :=
 { norm_mul := op_norm_comp_le,
   .. continuous_linear_map.to_normed_group }
 
-/-- For a nonzero normed space `E`, continuous linear endomorphisms form a normed algebra with
-respect to the operator norm. -/
-instance to_normed_algebra [nontrivial E] : normed_algebra 𝕜 (E →L[𝕜] E) :=
-{ norm_algebra_map_eq := λ c, show ∥c • id 𝕜 E∥ = ∥c∥,
-    by {rw [norm_smul, norm_id], simp},
-  .. continuous_linear_map.algebra }
-
 variable {f}
 
 lemma homothety_norm [ring_hom_isometric σ₁₂] [nontrivial E] (f : E →SL[σ₁₂] F) {a : ℝ}
@@ -1591,10 +1597,10 @@ continuous_linear_map.homothety_norm _ c.norm_smul_right_apply
 
 variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
 
-@[simp] lemma op_norm_lmul : ∥lmul 𝕜 𝕜'∥ = 1 :=
-by haveI := normed_algebra.nontrivial 𝕜 𝕜'; exact (lmulₗᵢ 𝕜 𝕜').norm_to_continuous_linear_map
+@[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_lmul_right : ∥lmul_right 𝕜 𝕜'∥ = 1 :=
+@[simp] lemma op_norm_lmul_right [norm_one_class 𝕜'] : ∥lmul_right 𝕜 𝕜'∥ = 1 :=
 (op_norm_flip (@lmul 𝕜 _ 𝕜' _ _)).trans (op_norm_lmul _ _)
 
 end continuous_linear_map