Faithfulness of Scalar Multiplication on Completions

Given a field K with an R-scalar multiplication, if the scalar action of R on K is faithful, then the induced scalar action of R on the completion of K is also faithful.

instance UniformSpace.Completion.faithfulSMul {R : Type u_1} {K : Type u_2} [CommSemiring R] [Field K] [Algebra R K] [UniformSpace K] [UniformContinuousConstSMul R K] [IsUniformAddGroup K] [IsTopologicalRing K] [Nontrivial (Completion K)] [FaithfulSMul R K] : FaithfulSMul R (Completion K)