Continuous linear maps and quotients

Stream: Is there code for X?

[Sebastien Gouezel]

I can't find the fact that a continuous linear map induces a continuous linear map on the quotient by its kernel. Is it really missing?

[Antoine Chambert-Loir]

It doesn't seem to exist, indeed. In fact, only a few file seem to mention such quotients. Mathlib.Topology.Algebra.Module.Basic says a bit about this quotient, docs#Submodule.topologicalAddGroup_quotient, for example that it is a topological additive group, and docs#Submodule.continuousSMul_quotient that it has a continuous multiplication. But that file isn't imported by many other ones and none of them seem to use quotients…