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.