refactor(topology/algebra/normed_group): generalize to semi_normed_group (#7066)

The completion of a `semi_normed_group` is a `normed_group` (and similarly for `pseudo_metric_space`).

Author: riccardobrasca

src/topology/algebra/normed_group.lean

@@ -29,11 +29,11 @@ instance [uniform_space V] [has_norm V] :
   has_norm (completion V) :=
 { norm := completion.extension has_norm.norm }
 
-@[simp] lemma norm_coe {V} [normed_group V] (v : V) :
+@[simp] lemma norm_coe {V} [semi_normed_group V] (v : V) :
   ∥(v : completion V)∥ = ∥v∥ :=
 completion.extension_coe uniform_continuous_norm v
 
-instance [normed_group V] : normed_group (completion V) :=
+instance [semi_normed_group V] : normed_group (completion V) :=
 { dist_eq :=
   begin
     intros x y,

src/topology/metric_space/completion.lean

@@ -20,7 +20,7 @@ open_locale filter
 noncomputable theory
 
 universes u
-variables {α : Type u} [metric_space α]
+variables {α : Type u} [pseudo_metric_space α]
 
 namespace metric
 
@@ -165,7 +165,7 @@ protected lemma completion.uniformity_dist :
   uniformity (completion α) = (⨅ ε>0, 𝓟 {p | dist p.1 p.2 < ε}) :=
 by simpa [infi_subtype] using @completion.uniformity_dist' α _
 
-/-- Metric space structure on the completion of a metric space. -/
+/-- Metric space structure on the completion of a pseudo_metric space. -/
 instance completion.metric_space : metric_space (completion α) :=
 { dist_self          := completion.dist_self,
   eq_of_dist_eq_zero := completion.eq_of_dist_eq_zero,