def Subring.toSubmodule {R : Type u_1} [Ring R] (S : Subring R) : Submodule (↥S) R

If S is a subring of R, then S can be viewed as an S-submodule of R.