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
@[simp]
Mathlib.Analysis.Normed.Group.Completion
In this file we prove that the completion of a (semi)normed group is a normed group.
normed group, completion