le.to_submodule

Stream: Is there code for X?

[Nicolò Cavalleri]

I might have forgotten how to search but I cannot find anything like this:

def le.to_submodule {R : Type*} [semiring R] (M : Type*) [add_comm_monoid M] [module R M] {p p' : submodule R M}
  (h : p ≤ p') : submodule R p' := (⊤ : submodule R p).map (submodule.of_le h)

Does it already exist?

[Adam Topaz]

you can use docs#submodule.comap and docs#submodule.subtype

[Adam Topaz]

your h isn't even needed, and you will end up with the intersection of p and p' (as a submodule of p')