Linear algebra question

Stream: maths

[Yury G. Kudryashov]

Hi, do we have extend_linear_map (M : submodule R V) {x : V} (hx : x ∉ M) (f : M →ₗ[R] V') (y : V') : (M ⊔ (submodule.span R {x})) →ₗ[R] V'?

[Kenny Lau]

consider V = V' = Z, M = 2Z, f(m) = m/2, y=1

[Yury G. Kudryashov]

OK, let's say k instead of R, and k is a field.

[Yury G. Kudryashov]

I'm interested in the case of vector spaces over real numbers.