Theorems · Inductive type · functional analysis

IsModuleTopology

(R : Type u_1) → [TopologicalSpace R] → (A : Type u_2) → [Add A] → [SMul R A] → [τA : TopologicalSpace A] → Prop

A class asserting that the topology on a module over a topological ring R is the module topology. See moduleTopology for more discussion of the module topology.

Defined in

Mathlib.Topology.Algebra.Module.ModuleTopology

Cited by

28 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceAddSMulTopologicalSpace