If E is a normed space over 𝕜, then so is uniform_space.completion E. In this file we provide
necessary instances and define uniform_space.completion.to_complₗᵢ - coercion
E → uniform_space.completion E as a bundled linear isometry.
E → uniform_space.completion E
Embedding of a normed space to its completion as a linear isometry.
Embedding of a normed space to its completion as a continuous linear map.