Commit 2026-05-19 15:28 da121d26

feat(Topology/Algebra/Module/Complement): bundle prodEquivOfIsCompl and quotientEquivOfIsCompl, add ContinuousLinearMap.ofIsTopCompl (#39260) This PR completes the three TODO items listed at the top of Mathlib/Topology/Algebra/Module/Complement.lean (introduced in #38547). Submodule.prodEquivOfIsCompl is shown to be a homeomorphism if and only if the two submodules are topological complements. The analogous characterisation for Submodule.quotientEquivOfIsCompl is also provided, and ContinuousLinearMap.ofIsTopCompl is defined as the continuous version of LinearMap.ofIsCompl, taking continuous linear maps from complementary submodules and producing the induced continuous linear map on the whole space.