feat(analysis/normed_space): normed_algebra.to_topological_algebra (#6779)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/analysis/normed_space/basic.lean

@@ -5,6 +5,7 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 import topology.instances.nnreal
 import topology.algebra.module
+import topology.algebra.algebra
 import topology.metric_space.antilipschitz
 
 /-!
@@ -294,7 +295,7 @@ lipschitz_on_with_iff_norm_sub_le.mp h x x_in y y_in
 /-- A homomorphism `f` of normed groups is continuous, if there exists a constant `C` such that for
 all `x`, one has `∥f x∥ ≤ C * ∥x∥`.
 The analogous condition for a linear map of normed spaces is in `normed_space.operator_norm`. -/
-lemma add_monoid_hom.continuous_of_bound (f :α →+ β) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
+lemma add_monoid_hom.continuous_of_bound (f : α →+ β) (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   continuous f :=
 (f.lipschitz_of_bound C h).continuous
 
@@ -1188,6 +1189,21 @@ normed_algebra.norm_algebra_map_eq _
 variables (𝕜 : Type*) [normed_field 𝕜]
 variables (𝕜' : Type*) [normed_ring 𝕜']
 
+-- This could also be proved via `linear_map.continuous_of_bound`,
+-- but this is further up the import tree in `normed_space.operator_norm`, so not yet available.
+@[continuity] lemma normed_algebra.algebra_map_continuous
+  [normed_algebra 𝕜 𝕜'] :
+  continuous (algebra_map 𝕜 𝕜') :=
+begin
+  change continuous (algebra_map 𝕜 𝕜').to_add_monoid_hom,
+  exact add_monoid_hom.continuous_of_bound _ 1 (λ x, by simp),
+end
+
+@[priority 100]
+instance normed_algebra.to_topological_algebra [normed_algebra 𝕜 𝕜'] :
+  topological_algebra 𝕜 𝕜' :=
+⟨by continuity⟩
+
 @[priority 100]
 instance normed_algebra.to_normed_space [h : normed_algebra 𝕜 𝕜'] : normed_space 𝕜 𝕜' :=
 { norm_smul_le := λ s x, calc