English
If N ⊆ O, then φ.submoduleImage N = range (φ ∘ inclusion h).
Русский
Если N ⊆ O, то φ.submoduleImage N = range (φ ∘ inclusion h).
LaTeX
$$$$ \varphi.\mathrm{submoduleImage }N = \operatorname{range}(\varphi \circ (\mathrm{inclusion}\; h)) $$$$
Lean4
/-- If `O` is a submodule of `M`, and `Φ : O →ₗ M'` is a linear map,
then `(ϕ : O →ₗ M').submoduleImage N` is `ϕ(N)` as a submodule of `M'` -/
def submoduleImage {M' : Type*} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} (ϕ : O →ₗ[R] M')
(N : Submodule R M) : Submodule R M' :=
(N.comap O.subtype).map ϕ