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]
theorem uniform_space.completion.norm_coe {E : Type u_1} [semi_normed_group E] (x : E) :