# Commit 2020-05-01 05:59 74d24aba

View on Github →feat(topology/instances/real_vector_space): `E →+ F`

to `E →L[ℝ] F`

(#2577)
A continuous additive map between two vector spaces over `ℝ`

is `ℝ`

-linear.

Mathlib v3 is deprecated. Go to Mathlib v4

feat(topology/instances/real_vector_space): `E →+ F`

to `E →L[ℝ] F`

(#2577)
A continuous additive map between two vector spaces over `ℝ`

is `ℝ`

-linear.