# Documentation

Mathlib.Topology.Instances.RealVectorSpace

# 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 map_real_smul {E : Type u_1} [] [] [] [] {F : Type u_2} [] [] [] [] [] {G : Type u_3} [] (f : G) (hf : ) (c : ) (x : E) :
f (c x) = c f x

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

def AddMonoidHom.toRealLinearMap {E : Type u_1} [] [] [] [] {F : Type u_2} [] [] [] [] [] (f : E →+ F) (hf : ) :

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

Instances For
@[simp]
theorem AddMonoidHom.coe_toRealLinearMap {E : Type u_1} [] [] [] [] {F : Type u_2} [] [] [] [] [] (f : E →+ F) (hf : ) :
↑() = f
def AddEquiv.toRealLinearEquiv {E : Type u_1} [] [] [] [] {F : Type u_2} [] [] [] [] [] (e : E ≃+ F) (h₁ : ) (h₂ : ) :

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

Instances For
instance Real.isScalarTower {E : Type u_1} [] [] [] [] [] {A : Type u_3} [] [Ring A] [] [Module A 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.