English
If E is a topological module over both a topological ℝ-algebra A and over ℝ, then the scalar actions are compatible; i.e., (r a) · x = a · (r · x) for all r ∈ ℝ, a ∈ A, x ∈ E.
Русский
Пусть E является топологической модулю над двумя структурами: топологической ℝ-алгеброй A и ℝ. Тогда скалярные действия совместимы: (r a) · x = a · (r · x) для всех r ∈ ℝ, a ∈ A, x ∈ E.
LaTeX
$$$\\forall r\\in\\mathbb{R},\\forall a\\in A,\\forall x\\in E:\\ (r a)\\cdot x = a\\cdot (r\\cdot x).$$$
Lean4
/-- 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. -/
instance (priority := 900) isScalarTower [T2Space E] {A : Type*} [TopologicalSpace A] [Ring A] [Algebra ℝ A]
[Module A E] [ContinuousSMul ℝ A] [ContinuousSMul A E] : IsScalarTower ℝ A E :=
⟨fun r x y => map_real_smul ((smulAddHom A E).flip y) (continuous_id.smul continuous_const) r x⟩
