diff --git a/src/analysis/complex/basic.lean b/src/analysis/complex/basic.lean
index 98e96f07a2f78..378408840be86 100644
--- a/src/analysis/complex/basic.lean
+++ b/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| :=
diff --git a/src/analysis/normed/normed_field.lean b/src/analysis/normed/normed_field.lean
index 5b624a897991a..2247519ba7780 100644
--- a/src/analysis/normed/normed_field.lean
+++ b/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. -/
diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 2c50fa293e94b..35fffc9a63514 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/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
diff --git a/src/analysis/normed_space/is_R_or_C.lean b/src/analysis/normed_space/is_R_or_C.lean
index 5869ae7edd1c5..d0d42de322ac4 100644
--- a/src/analysis/normed_space/is_R_or_C.lean
+++ b/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]
 
diff --git a/src/analysis/normed_space/operator_norm.lean b/src/analysis/normed_space/operator_norm.lean
index 8e8456d198aef..2cc99c0cc9cd5 100644
--- a/src/analysis/normed_space/operator_norm.lean
+++ b/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,25 +780,27 @@ 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. -/
@@ -800,19 +808,22 @@ def lmul_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' := (lmul 𝕜 𝕜').fl
 
 @[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
diff --git a/src/analysis/normed_space/spectrum.lean b/src/analysis/normed_space/spectrum.lean
index 36caf279fb412..6ae2ba0bc0099 100644
--- a/src/analysis/normed_space/spectrum.lean
+++ b/src/analysis/normed_space/spectrum.lean
@@ -70,12 +70,12 @@ not_not.mp $ λ hn, h.not_le $ le_supr₂ k hn
 variable [complete_space A]
 
 lemma is_open_resolvent_set (a : A) : is_open (ρ a) :=
-units.is_open.preimage ((algebra_map_isometry 𝕜 A).continuous.sub continuous_const)
+units.is_open.preimage ((algebra_map_clm 𝕜 A).continuous.sub continuous_const)
 
 lemma is_closed (a : A) : is_closed (σ a) :=
 (is_open_resolvent_set a).is_closed_compl
 
-lemma mem_resolvent_of_norm_lt {a : A} {k : 𝕜} (h : ∥a∥ < ∥k∥) :
+lemma mem_resolvent_of_norm_lt [norm_one_class A] {a : A} {k : 𝕜} (h : ∥a∥ < ∥k∥) :
   k ∈ ρ a :=
 begin
   rw [resolvent_set, set.mem_set_of_eq, algebra.algebra_map_eq_smul_one],
@@ -85,28 +85,28 @@ begin
   simpa [ku, sub_eq_add_neg, algebra.algebra_map_eq_smul_one] using (ku.add (-a) hku).is_unit,
 end
 
-lemma norm_le_norm_of_mem {a : A} {k : 𝕜} (hk : k ∈ σ a) :
+lemma norm_le_norm_of_mem [norm_one_class A] {a : A} {k : 𝕜} (hk : k ∈ σ a) :
   ∥k∥ ≤ ∥a∥ :=
 le_of_not_lt $ mt mem_resolvent_of_norm_lt hk
 
-lemma subset_closed_ball_norm (a : A) :
+lemma subset_closed_ball_norm [norm_one_class A] (a : A) :
   σ a ⊆ metric.closed_ball (0 : 𝕜) (∥a∥) :=
 λ k hk, by simp [norm_le_norm_of_mem hk]
 
-lemma is_bounded (a : A) : metric.bounded (σ a) :=
+lemma is_bounded [norm_one_class A] (a : A) : metric.bounded (σ a) :=
 (metric.bounded_iff_subset_ball 0).mpr ⟨∥a∥, subset_closed_ball_norm a⟩
 
-theorem is_compact [proper_space 𝕜] (a : A) : is_compact (σ a) :=
+theorem is_compact [norm_one_class A] [proper_space 𝕜] (a : A) : is_compact (σ a) :=
 metric.is_compact_of_is_closed_bounded (is_closed a) (is_bounded a)
 
-theorem spectral_radius_le_nnnorm (a : A) :
+theorem spectral_radius_le_nnnorm [norm_one_class A] (a : A) :
   spectral_radius 𝕜 a ≤ ∥a∥₊ :=
 by { refine supr₂_le (λ k hk, _), exact_mod_cast norm_le_norm_of_mem hk }
 
 open ennreal polynomial
 
 variable (𝕜)
-theorem spectral_radius_le_pow_nnnorm_pow_one_div (a : A) (n : ℕ) :
+theorem spectral_radius_le_pow_nnnorm_pow_one_div [norm_one_class A] (a : A) (n : ℕ) :
   spectral_radius 𝕜 a ≤ ∥a ^ (n + 1)∥₊ ^ (1 / (n + 1) : ℝ) :=
 begin
   refine supr₂_le (λ k hk, _),
@@ -282,7 +282,7 @@ end
 
 /-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
 `spectral_radius` of `a` is the limit of the sequence `∥a ^ n∥₊ ^ (1 / n)` -/
-theorem pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius (a : A) :
+theorem pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius [norm_one_class A] (a : A) :
   tendsto (λ n : ℕ, ((∥a ^ n∥₊ ^ (1 / n : ℝ)) : ℝ≥0∞)) at_top (𝓝 (spectral_radius ℂ a)) :=
 begin
   refine tendsto_of_le_liminf_of_limsup_le _ _ (by apply_auto_param) (by apply_auto_param),
@@ -296,7 +296,7 @@ end
 instead of `nnnorm`. -/
 /-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
 `spectral_radius` of `a` is the limit of the sequence `∥a ^ n∥₊ ^ (1 / n)` -/
-theorem pow_norm_pow_one_div_tendsto_nhds_spectral_radius (a : A) :
+theorem pow_norm_pow_one_div_tendsto_nhds_spectral_radius [norm_one_class A] (a : A) :
   tendsto (λ n : ℕ,  ennreal.of_real (∥a ^ n∥ ^ (1 / n : ℝ))) at_top (𝓝 (spectral_radius ℂ a)) :=
 begin
   convert pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius a,
@@ -414,11 +414,12 @@ local notation `↑ₐ` := algebra_map 𝕜 A
 
 /-- An algebra homomorphism into the base field, as a continuous linear map (since it is
 automatically bounded). -/
-@[simps] def to_continuous_linear_map (φ : A →ₐ[𝕜] 𝕜) : A →L[𝕜] 𝕜 :=
+@[simps] def to_continuous_linear_map [norm_one_class A] (φ : A →ₐ[𝕜] 𝕜) : A →L[𝕜] 𝕜 :=
 φ.to_linear_map.mk_continuous_of_exists_bound $
   ⟨1, λ a, (one_mul ∥a∥).symm ▸ spectrum.norm_le_norm_of_mem (φ.apply_mem_spectrum _)⟩
 
-lemma continuous (φ : A →ₐ[𝕜] 𝕜) : continuous φ := φ.to_continuous_linear_map.continuous
+lemma continuous [norm_one_class A] (φ : A →ₐ[𝕜] 𝕜) : continuous φ :=
+φ.to_continuous_linear_map.continuous
 
 end normed_field
 
diff --git a/src/analysis/normed_space/star/spectrum.lean b/src/analysis/normed_space/star/spectrum.lean
index ca708c04d7fca..8110678ab8ca1 100644
--- a/src/analysis/normed_space/star/spectrum.lean
+++ b/src/analysis/normed_space/star/spectrum.lean
@@ -51,7 +51,8 @@ variables {A : Type*}
 
 local notation `↑ₐ` := algebra_map ℂ A
 
-lemma spectral_radius_eq_nnnorm_of_self_adjoint {a : A} (ha : a ∈ self_adjoint A) :
+lemma spectral_radius_eq_nnnorm_of_self_adjoint [norm_one_class A] {a : A}
+  (ha : a ∈ self_adjoint A) :
   spectral_radius ℂ a = ∥a∥₊ :=
 begin
   have hconst : tendsto (λ n : ℕ, (∥a∥₊ : ℝ≥0∞)) at_top _ := tendsto_const_nhds,
@@ -64,7 +65,7 @@ begin
   simp,
 end
 
-lemma spectral_radius_eq_nnnorm_of_star_normal (a : A) [is_star_normal a] :
+lemma spectral_radius_eq_nnnorm_of_star_normal [norm_one_class A] (a : A) [is_star_normal a] :
   spectral_radius ℂ a = ∥a∥₊ :=
 begin
   refine (ennreal.pow_strict_mono (by linarith : 2 ≠ 0)).injective _,
diff --git a/src/analysis/quaternion.lean b/src/analysis/quaternion.lean
index c5fdbf03e0ca9..2b77f49fb5427 100644
--- a/src/analysis/quaternion.lean
+++ b/src/analysis/quaternion.lean
@@ -57,7 +57,7 @@ instance : norm_one_class ℍ :=
 @[simp, norm_cast] lemma norm_coe (a : ℝ) : ∥(a : ℍ)∥ = ∥a∥ :=
 by rw [norm_eq_sqrt_real_inner, inner_self, norm_sq_coe, real.sqrt_sq_eq_abs, real.norm_eq_abs]
 
-@[simp, norm_cast] lemma nnorm_coe (a : ℝ) : ∥(a : ℍ)∥₊ = ∥a∥₊ :=
+@[simp, norm_cast] lemma nnnorm_coe (a : ℝ) : ∥(a : ℍ)∥₊ = ∥a∥₊ :=
 subtype.ext $ norm_coe a
 
 noncomputable instance : normed_division_ring ℍ :=
@@ -66,7 +66,7 @@ noncomputable instance : normed_division_ring ℍ :=
                            exact real.sqrt_mul norm_sq_nonneg _ } }
 
 noncomputable instance : normed_algebra ℝ ℍ :=
-{ norm_algebra_map_eq := norm_coe,
+{ norm_smul_le := λ a x, (norm_smul a x).le,
   to_algebra := quaternion.algebra }
 
 instance : has_coe ℂ ℍ := ⟨λ z, ⟨z.re, z.im, 0, 0⟩⟩
diff --git a/src/number_theory/cyclotomic/discriminant.lean b/src/number_theory/cyclotomic/discriminant.lean
index 0357923fc6b19..1c8bb0fe92095 100644
--- a/src/number_theory/cyclotomic/discriminant.lean
+++ b/src/number_theory/cyclotomic/discriminant.lean
@@ -119,7 +119,7 @@ begin
       { exact hζ.pow_sub_one_norm_prime_pow_of_one_le hirr (by simpa using hirr₁) rfl.le (hp2 hp) },
       { exact hζ.pow_sub_one_norm_prime_ne_two hirr (by simpa using hirr₁) rfl.le hp } },
     rw [monoid_hom.map_mul, hnorm, monoid_hom.map_mul, ← map_nat_cast (algebra_map K L),
-      norm_algebra_map, finrank _ hirr, pnat.pow_coe, totient_prime_pow hp.out (succ_pos k),
+      algebra.norm_algebra_map, finrank _ hirr, pnat.pow_coe, totient_prime_pow hp.out (succ_pos k),
       nat.sub_one, nat.pred_succ, ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow,
       hζ.norm_eq_one hk hirr, one_pow, mul_one, cast_pow, ← coe_coe, ← pow_mul, ← mul_assoc,
       mul_comm (k + 1), mul_assoc] at H,
diff --git a/src/number_theory/cyclotomic/primitive_roots.lean b/src/number_theory/cyclotomic/primitive_roots.lean
index 29d8cd386519e..ce0960555630a 100644
--- a/src/number_theory/cyclotomic/primitive_roots.lean
+++ b/src/number_theory/cyclotomic/primitive_roots.lean
@@ -184,7 +184,8 @@ variables {K} [field K] [algebra K L] [ne_zero ((n : ℕ) : K)]
 
 /-- This mathematically trivial result is complementary to `norm_eq_one` below. -/
 lemma norm_eq_neg_one_pow (hζ : is_primitive_root ζ 2) : norm K ζ = (-1) ^ finrank K L :=
-by rw [hζ.eq_neg_one_of_two_right , show -1 = algebra_map K L (-1), by simp, norm_algebra_map]
+by rw [hζ.eq_neg_one_of_two_right , show -1 = algebra_map K L (-1), by simp,
+  algebra.norm_algebra_map]
 
 include hζ
 
@@ -195,7 +196,7 @@ lemma norm_eq_one [is_cyclotomic_extension {n} K L] (hn : n ≠ 2)
 begin
   by_cases h1 : n = 1,
   { rw [h1, one_coe, one_right_iff] at hζ,
-    rw [hζ, show 1 = algebra_map K L 1, by simp, norm_algebra_map, one_pow] },
+    rw [hζ, show 1 = algebra_map K L 1, by simp, algebra.norm_algebra_map, one_pow] },
   { replace h1 : 2 ≤ n,
     { by_contra' h,
       exact h1 (pnat.eq_one_of_lt_two h) },
@@ -211,7 +212,7 @@ lemma norm_eq_one_of_linearly_ordered {K : Type*} [linear_ordered_field K] [alge
 begin
   haveI := ne_zero.of_no_zero_smul_divisors K L n,
   have hz := congr_arg (norm K) ((is_primitive_root.iff_def _ n).1 hζ).1,
-  rw [←(algebra_map K L).map_one , norm_algebra_map, one_pow, map_pow, ←one_pow ↑n] at hz,
+  rw [←(algebra_map K L).map_one , algebra.norm_algebra_map, one_pow, map_pow, ←one_pow ↑n] at hz,
   exact strict_mono.injective hodd.strict_mono_pow hz
 end
 
@@ -412,7 +413,8 @@ begin
   { simp only [_root_.map_neg, map_bit0, _root_.map_one],
     ring },
   replace hirr : irreducible (cyclotomic (2 ^ (k + 1) : ℕ+) K) := by simp [hirr],
-  rw [this.eq_neg_one_of_two_right, H, norm_algebra_map, is_cyclotomic_extension.finrank L hirr,
+  rw [this.eq_neg_one_of_two_right, H, algebra.norm_algebra_map,
+    is_cyclotomic_extension.finrank L hirr,
     pow_coe, pnat.coe_bit0, one_coe, totient_prime_pow nat.prime_two (zero_lt_succ k),
     succ_sub_succ_eq_sub, tsub_zero, mul_one]
 end
diff --git a/src/ring_theory/norm.lean b/src/ring_theory/norm.lean
index 298a66638e7ce..044e4098ad177 100644
--- a/src/ring_theory/norm.lean
+++ b/src/ring_theory/norm.lean
@@ -89,7 +89,7 @@ end
 (If `L` is not finite-dimensional over `K`, then `norm = 1 = x ^ 0 = x ^ (finrank L K)`.)
 -/
 @[simp]
-lemma norm_algebra_map (x : K) : norm K (algebra_map K L x) = x ^ finrank K L :=
+protected lemma norm_algebra_map (x : K) : norm K (algebra_map K L x) = x ^ finrank K L :=
 begin
   by_cases H : ∃ (s : finset L), nonempty (basis s K L),
   { rw [norm_algebra_map_of_basis H.some_spec.some, finrank_eq_card_basis H.some_spec.some] },
diff --git a/src/ring_theory/polynomial/eisenstein.lean b/src/ring_theory/polynomial/eisenstein.lean
index 13c457b336a18..9c7ab6a9d8edb 100644
--- a/src/ring_theory/polynomial/eisenstein.lean
+++ b/src/ring_theory/polynomial/eisenstein.lean
@@ -357,12 +357,12 @@ begin
           p • Q.coeff x • f (x + n))
     : congr_arg (norm K) (eq_sub_of_add_eq _)
   ... = _ : _,
-  { simp only [algebra.smul_def, algebra_map_apply R K L, norm_algebra_map, _root_.map_mul,
+  { simp only [algebra.smul_def, algebra_map_apply R K L, algebra.norm_algebra_map, _root_.map_mul,
       _root_.map_pow, finrank_K_L, power_basis.norm_gen_eq_coeff_zero_minpoly,
       minpoly.gcd_domain_eq_field_fractions K hBint, coeff_map, ← hn],
     ring_exp },
   swap, { simp_rw [← smul_sum, ← smul_sub, algebra.smul_def p, algebra_map_apply R K L,
-      _root_.map_mul, norm_algebra_map, finrank_K_L, hr, ← hn] },
+      _root_.map_mul, algebra.norm_algebra_map, finrank_K_L, hr, ← hn] },
 
   calc _ = (Q.coeff 0 • 1 + ∑ (x : ℕ) in (range (Q.nat_degree + 1)).erase 0,
               Q.coeff x • B.gen ^ x) * B.gen ^ n : _
@@ -529,7 +529,8 @@ begin
         simpa using hk } },
     obtain ⟨r, hr⟩ := is_integral_iff.1 (is_integral_norm K hintsum),
     rw [algebra.smul_def, mul_assoc, ← mul_sub, _root_.map_mul, algebra_map_apply R K L, map_pow,
-      norm_algebra_map, _root_.map_mul, algebra_map_apply R K L, norm_algebra_map, finrank B, ← hr,
+      algebra.norm_algebra_map, _root_.map_mul, algebra_map_apply R K L, algebra.norm_algebra_map,
+      finrank B, ← hr,
       power_basis.norm_gen_eq_coeff_zero_minpoly, minpoly.gcd_domain_eq_field_fractions K hBint,
       coeff_map, show (-1 : K) = algebra_map R K (-1), by simp, ← map_pow, ← map_pow,
       ← _root_.map_mul, ← map_pow, ← _root_.map_mul, ← map_pow, ← _root_.map_mul] at hQ,
diff --git a/src/topology/continuous_function/bounded.lean b/src/topology/continuous_function/bounded.lean
index 13c2843ff26b2..3c92c051eed18 100644
--- a/src/topology/continuous_function/bounded.lean
+++ b/src/topology/continuous_function/bounded.lean
@@ -1119,13 +1119,8 @@ instance : algebra 𝕜 (α →ᵇ γ) :=
   algebra_map 𝕜 (α →ᵇ γ) k a = k • 1 :=
 by { rw algebra.algebra_map_eq_smul_one, refl, }
 
-instance [nonempty α] : normed_algebra 𝕜 (α →ᵇ γ) :=
-{ norm_algebra_map_eq := λ c, begin
-    calc ∥ (algebra_map 𝕜 (α →ᵇ γ)).to_fun c∥ = ∥(algebra_map 𝕜 γ) c∥ : _
-    ... = ∥c∥ : norm_algebra_map_eq _ _,
-    apply norm_const_eq ((algebra_map 𝕜 γ) c), assumption,
-  end,
-  ..bounded_continuous_function.algebra }
+instance : normed_algebra 𝕜 (α →ᵇ γ) :=
+{ ..bounded_continuous_function.normed_space }
 
 /-!
 ### Structure as normed module over scalar functions
diff --git a/src/topology/continuous_function/compact.lean b/src/topology/continuous_function/compact.lean
index 88de16c29ca02..30844763f0d4d 100644
--- a/src/topology/continuous_function/compact.lean
+++ b/src/topology/continuous_function/compact.lean
@@ -258,8 +258,8 @@ end
 section
 variables {𝕜 : Type*} {γ : Type*} [normed_field 𝕜] [normed_ring γ] [normed_algebra 𝕜 γ]
 
-instance [nonempty α] : normed_algebra 𝕜 C(α, γ) :=
-{ norm_algebra_map_eq := λ c, (norm_algebra_map_eq (α →ᵇ γ) c : _), }
+instance : normed_algebra 𝕜 C(α, γ) :=
+{ ..continuous_map.normed_space }
 
 end