Image of a linear map

Stream: new members

[Maxime Darrin]

Hi !
I'm trying to write the image of a linear map.

import algebra.module.linear_map
import linear_algebra.basic
import data.real.basic
import algebra.module.submodule

example
(R : Type*) (E : Type*) (F : Type*)
[semiring R]
[add_comm_monoid E] [module R E]
(f  : linear_map R E E)
:
f  '' E  := sorry

example
(R : Type*) (E : Type*) (F : Type*)
[semiring R]
[add_comm_monoid E] [module R E]
(f  : linear_map R E E)
:
f  '' \top  := sorry

In the second case it works but the results is not a submodule. How can I get Im f as a submodule ?

Thanks for the help!

[Kevin Buzzard]

example (R : Type*) (E : Type*) (F : Type*)
  [semiring R] [add_comm_monoid E] [module R E]
  (f  : E →ₗ[R] E) : submodule R E :=
(⊤ : submodule R E).map f

[Kevin Buzzard]

E →ₗ[R] E is notation for linear_map R E E, submodule.map is pushforward of submodules along a linear map, and ⊤ (top, not T) is the biggest submodule. I am rather surprised that there is no submodule.range.

[Eric Wieser]

docs#linear_map.range

[Kevin Buzzard]

But docs#submodule.map ?

[Kevin Buzzard]

I guess it makes sense