Normed space structure on the completion of a normed space

We show that the completion of a normed and completable topological field is also a normed field.

noncomputable instance UniformSpace.Completion.instNormedFieldOfCompletableTopField (A : Type u_1) [NormedField A] [CompletableTopField A] : NormedField (UniformSpace.Completion A)

Equations

• UniformSpace.Completion.instNormedFieldOfCompletableTopField A = NormedField.mk ⋯ ⋯