submodule of a submodule

Stream: Is there code for X?

[Scott Morrison]

import algebra.module.submodule

example (R M : Type) [ring R] [add_comm_group M] [module R M]
  (A : submodule R M) (B : submodule R A) :
  submodule R M := sorry -- B as a submodule of M?

[Johan Commelin]

Is it something like B.map A.incl?

[Kevin Buzzard]

For subgroups the morphism is A.subtype

[Eric Wieser]

That seems to be the preferred spelling, given how docs#submodule.equiv_subtype_map is stated