2026-05-19 15:28
Mathlib/Topology/Algebra/Module/Complement.lean
feat(Topology/Algebra/Module/Complement): bundle `prodEquivOfIsCompl` and `quotientEquivOfIsCompl`, add `ContinuousLinearMap.ofIsTopCompl` (#39260) …
Added ContinuousLinearMap.toLinearMap_ofIsTopCompl