IsTopologicalModule

📁 Source: FLT/Deformations/ContinuousRepresentation/IsTopologicalModule.lean

Statistics

Metric	Count
Definitions IsTopologicalModule	1
Theorems toContinuousAdd, toContinuousSMul, instTopologicalModule, instIsTopologicalModuleSubtypeMem, topologicalModule	5
Total	6

IsTopologicalModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContinuousAdd 📖	—	—	—	—	—
toContinuousSMul 📖	—	—	—	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTopologicalModule 📖	—	IsTopologicalModule	—	—	IsTopologicalModule.toContinuousSMul IsTopologicalModule.toContinuousAdd

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTopologicalModuleSubtypeMem 📖	mathematical	—	IsTopologicalModule	—	Topology.IsInducing.topologicalModule

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topologicalModule 📖	mathematical	—	IsTopologicalModule	—	IsTopologicalModule.toContinuousSMul IsTopologicalModule.toContinuousAdd

(root)

Definitions

Name	Category	Theorems
IsTopologicalModule 📖	CompData	4 math math: Submodule.instIsTopologicalModuleSubtypeMem, Topology.IsInducing.topologicalModule, IsModuleTopology.iff_Continuous_algebraMap, IsModuleTopology.isTopologicalModule

---

← Back to Index