Theorem Submodule.coe_projectionL

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_projectionLView on Github →