(continous) linear_maps between `p` and `p.restrict_scalars`

Stream: Is there code for X?

[Eric Wieser]

For [is_scalar_tower S R M] [semimodule R M] [semimodule S M] (p : submodule R M), do we have any of the following maps between p and docs#submodule.restrict_scalars?
*↥(p.restrict_scalars S) ≃ₗ[S] ↥p
*↥(p.restrict_scalars S) ≃L[S] ↥p
*↥(p.restrict_scalars S) →ₗ[S] ↥p
*↥(p.restrict_scalars S) →L[S] ↥p

I can get the third one from docs#submodule.of_le I expect, but I'm not sure about the others.