Theorem ModuleTopology.eq_coinduced_of_surjective

Modification history

2024-12-21 19:47
Mathlib/Topology/Algebra/Module/ModuleTopology.lean
feat(Topology/Algebra/Module/ModuleTopology): continuous linear surjections are quotient maps (#20012)
Added ModuleTopology.eq_coinduced_of_surjectiveView on Github →