Set is a submodule

Stream: Is there code for X?

[Wrenna Robson]

I notice that unbundled predicates like is_submonoid are deprecated. But I'm trying to capture the following: I have some map, not necessarily linear, which maps from an arbitrary type to a module. Suppose the range of the map admits a submodule structure (which does not necessarily come from the map itself). How do I express "this set admits a submodule", or "there is a submodule which has this set as its carrier"?

[Alex J. Best]

I think the second sentence should work, and has been used previously in mathlib \exists m : submodule M, S = m or something of that nature, if S is a set M and M is a module.

[Wrenna Robson]

Ah, if that's a useful form, then good good.