UniformSpace.Completion.norm_coe

theorem UniformSpace.Completion.norm_coe : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (x : E), ‖↑E x‖ = ‖x‖

This theorem states that for any type `E` which is a seminormed additive commutative group, the norm of an element `x` of `E` when it is embedded into the uniform space completion of `E` is equal to the norm of `x` in `E`. In other words, embedding a seminormed additive commutative group into its uniform space completion preserves the norm of its elements.

More concisely: The norm of an element in a seminormed additive commutative group is equal to its norm in the completion of that group under the embedding homomorphism.