Stream: maths

Topic: Linear algebra question

Yury G. Kudryashov (Jan 07 2020 at 02:02):

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 (Jan 07 2020 at 02:05):

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

Yury G. Kudryashov (Jan 07 2020 at 02:10):

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

Yury G. Kudryashov (Jan 07 2020 at 02:10):

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

Last updated: May 11 2021 at 17:39 UTC