Theorem IsModuleTopology.topologicalAddGroup

Modification history

2026-08-25 11:58

Mathlib/Topology/Algebra/Module/ModuleTopology.lean

chore: topologicalGroup -> isTopologicalGroup in names (#43027)

Deleted IsModuleTopology.topologicalAddGroup View on Github →

2024-12-21 19:47

Mathlib/Topology/Algebra/Module/ModuleTopology.lean

feat(Topology/Algebra/Module/ModuleTopology): continuous linear surjections are quotient maps (#20012)

Added IsModuleTopology.topologicalAddGroup View on Github →