Theorems · Definition · functional analysis

moduleTopology

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

The module topology, for a module A over a topological ring R. It's the finest topology making addition and the R-action continuous, or equivalently the finest topology making A into a topological R-module. More precisely it's the Inf of the set of topologies with these properties; theorems continuousSMul and continuousAdd show that the module topology also has these properties.

Defined in

Mathlib.Topology.Algebra.Module.ModuleTopology

Cited by

9 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddSMul