Theorem Submodule.coe_prodEquivOfIsTopCompl

Modification history

2026-06-10 10:22
Mathlib/Topology/Algebra/Module/Complement.lean
refactor(Analysis/Normed/Module/Complemented): add `IsCompl.isTopCompl_of_isClosed` and `isTopCompl_iff_isCompl_isClosed` (#39815) …
Added Submodule.coe_prodEquivOfIsTopComplView on Github →