Commit 2024-12-21 19:47 4c664176

View on Github →

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

Estimated changes

Modified Mathlib/Topology/Algebra/Module/ModuleTopology.lean

added theorem IsModuleTopology.continuousNeg

added theorem IsModuleTopology.isQuotientMap_of_surjective

added theorem IsModuleTopology.topologicalAddGroup

added theorem ModuleTopology.eq_coinduced_of_surjective