Commit 2026-05-10 22:54 50f0559a

feat: generalize Submodule.ClosedComplemented.of_quotient_finiteDimensional (#38579) Submodule.ClosedComplemented.of_quotient_finiteDimensional currently says that any finite codimension closed subspace of a Banach space is topologically complemented. The current proof uses the Banach open mapping theorem. In fact the result holds for any TVS over a nontrivially normed field, and we have the stronger result that any algebraic complement of a finite codimension closed subspace is in fact a topological complement.