mathlib documentation

analysis.normed.group.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

@[simp]