feat: port Analysis.Normed.Group.Completion (#2770)

Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib.lean

@@ -241,6 +241,7 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.Analysis.Normed.Group.Basic
+import Mathlib.Analysis.Normed.Group.Completion
 import Mathlib.Analysis.Normed.Group.Hom
 import Mathlib.Analysis.Normed.Group.InfiniteSum
 import Mathlib.Analysis.Normed.Group.Seminorm

Mathlib/Analysis/Normed/Group/Completion.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+
+! This file was ported from Lean 3 source module analysis.normed.group.completion
+! leanprover-community/mathlib commit 17ef379e997badd73e5eabb4d38f11919ab3c4b3
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Normed.Group.Basic
+import Mathlib.Topology.Algebra.GroupCompletion
+import Mathlib.Topology.MetricSpace.Completion
+
+/-!
+# Completion of a normed group
+
+In this file we prove that the completion of a (semi)normed group is a normed group.
+
+## Tags
+
+normed group, completion
+-/
+
+
+noncomputable section
+
+namespace UniformSpace
+
+namespace Completion
+
+variable (E : Type _)
+
+instance [UniformSpace E] [Norm E] : Norm (Completion E) where
+  norm := Completion.extension Norm.norm
+
+@[simp]
+theorem norm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖ = ‖x‖ :=
+  Completion.extension_coe uniformContinuous_norm x
+#align uniform_space.completion.norm_coe UniformSpace.Completion.norm_coe
+
+instance [SeminormedAddCommGroup E] : NormedAddCommGroup (Completion E) where
+  dist_eq x y := by
+    induction x, y using Completion.induction_on₂
+    · refine' isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous _
+      exact Continuous.comp Completion.continuous_extension continuous_sub
+    · rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]
+
+end Completion
+
+end UniformSpace