A normed field is a completable topological field

instance NormedField.instCompletableTopField {F : Type u_1} [NormedField F] : CompletableTopField F