## Stream: Is there code for X?

### Topic: (continous) linear_maps between p and p.restrict_scalars

#### Eric Wieser (Mar 15 2021 at 14:35):

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.

Last updated: May 07 2021 at 22:14 UTC