Theorem Submodule.IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl

Modification history

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 Submodule.IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl View on Github →