# Commit 2024-09-28 23:34 2845f11d

View on Github →feat(SeparationQuotient): add missing instances (#17239)
Also prove `SeparationQuotient.postcomp_mkCLM_surjective`

.
I'm going to need these instances and lemmas
to generalize `CompleteSpace (E →L[K] F)`

to topological vector spaces
without assuming that `F`

is a Hausdorff space, see #17244.