Completion of topological rings

This file contains a helper result for coercion within UniformSpace.extensionHom usage.

theorem UniformSpace.Completion.extensionHom_coe {α : Type u_1} [Ring α] [UniformSpace α] [TopologicalRing α] [UniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [UniformAddGroup β] [TopologicalRing β] (f : α →+* β) (hf : Continuous ⇑f) [CompleteSpace β] [T0Space β] (a : α) : (UniformSpace.Completion.extensionHom f hf) (↑α a) = f a