# mathlibdocumentation

topology.instances.real_vector_space

# Continuous additive maps are ℝ-linear #

In this file we prove that a continuous map f : E →+ F between two topological vector spaces over ℝ is ℝ-linear

theorem add_monoid_hom.map_real_smul {E : Type u_1} [ E] {F : Type u_2} [ F] [t2_space F] (f : E →+ F) (hf : continuous f) (c : ) (x : E) :
f (c x) = c f x

A continuous additive map between two vector spaces over ℝ is ℝ-linear.

def add_monoid_hom.to_real_linear_map {E : Type u_1} [ E] {F : Type u_2} [ F] [t2_space F] (f : E →+ F) (hf : continuous f) :

Reinterpret a continuous additive homomorphism between two real vector spaces as a continuous real-linear map.

Equations
@[simp]
theorem add_monoid_hom.coe_to_real_linear_map {E : Type u_1} [ E] {F : Type u_2} [ F] [t2_space F] (f : E →+ F) (hf : continuous f) :
def add_equiv.to_real_linear_equiv {E : Type u_1} [ E] {F : Type u_2} [ F] [t2_space F] (e : E ≃+ F) (h₁ : continuous e) (h₂ : continuous (e.symm)) :

Reinterpret a continuous additive equivalence between two real vector spaces as a continuous real-linear map.

Equations
@[protected, instance]
def real.is_scalar_tower {E : Type u_1} [ E] [t2_space E] {A : Type u_2} [ring A] [ A] [ E] [ E] :
E

A topological group carries at most one structure of a topological ℝ-module, so for any topological ℝ-algebra A (e.g. A = ℂ) and any topological group that is both a topological ℝ-module and a topological A-module, these structures agree.