NormedAddGroupHom.completion_coe'

theorem NormedAddGroupHom.completion_coe' : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) (g : G), UniformSpace.Completion.map (⇑f) (↑G g) = ↑H (f g)

This theorem states that for any two types `G` and `H` that are instances of the `SeminormedAddCommGroup` class, and given a normed additive group homomorphism `f` from `G` to `H`, the mapping of the completion of `G` to the completion of `H` by `f` is equal to the completion of the image of any element `g` of `G` under `f`. In other words, if we first complete `G` and then apply the homomorphism `f`, it's the same as if we first apply `f` and then complete.

More concisely: The completion of a normed additive group homomorphism between two seminormed additive groups is equal to the homomorphism of their completions.